Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.java.programmer > #53730

Re: ANN: Dogelog Player 1.2.0 (Binary Streams)

Show all headers | View raw

We have retracted our simple λμ-calculus blog
post until we have explored its model and proof
theory more thoroughly. Some of the model theory
has already been complete in a post on medium.com .
We here report on a puzzle stone in proof theory.

With the help of combinatorial logic,
unify_with_occurs_check/2 and a meta-interpreter
we can solve the type inhabitation problem brute
force in Prolog. This method is powerful enough
to assist us in a direct proof of Segerbergs 1968
result that JE = JP.

See also:

Segerberg Proofs in Dogelog Player
https://twitter.com/dogelogch/status/1810747113791442952

Segerberg Proofs in Dogelog Player
https://www.facebook.com/groups/dogelog

Mild Shock schrieb:
> 
> We have retracted our simple λμ-calculus blog
> post until we have explored its model and proof
> theory more thoroughly. Meanwhile we made a
> little tool that finds counter models for
> propositional formulas in a couple of
> intermediate logics between minimal logic
> and classical logic.
> 
> The easy part was McCunes Mace4 model finder
> and standard translation for propositional modal
> logic K and modal logic S4. We then opted for
> Segerbergs translation instead of Gödels translation,
> and could build model finders for minimal logic,
> Peirce’s logic and intuitionistic logic.
> 
> See also:
> 
> Segerberg Models in Dogelog Player
> https://twitter.com/dogelogch/status/1810177721239998611
> 
> Segerberg Models in Dogelog Player
> https://www.facebook.com/groups/dogelog
> 
> Mild Shock schrieb:
>>
>> Dogelog Player is a Prolog system that supports
>> JavaScript, Python and Java in its targets. We
>> show how the JavaScript support can be used to
>> perform some proof search and proof rendering
>> directly in the browser. A versatile format for
>> proof objects are λμ-expressions.
>>
>> We explored proof searches dubbed Dragalin and
>> Fitting, whereas the later outperforms the former.
>> The extracted λμ-expressions are used to display
>> Gentzen and Fitch style proofs. The Fitch style
>> proofs turn out to be more compact, but we are
>> still investigating some further reductions.
>>
>> See also:
>>
>> Simple λμ-Calculus in Dogelog Player
>> https://twitter.com/dogelogch/status/1803200066066456876
>>
>> Simple λμ-Calculus in Dogelog Player
>> https://www.facebook.com/groups/dogelog
>>
>> Mild Shock schrieb:
>>> Dear All,
>>>
>>> We are happy to announce a new edition
>>> of the Dogelog player:
>>>
>>> - Quasi-Parallel Loader:
>>>    The Prolog text loader is now task aware.
>>> Although tasks are only quasi-parallel, issues
>>> of mutex might appear, which have been solved
>>> by using the meta call shield/1 which temporarly
>>> disables auto-yield. Back traces showing the
>>> current file loading chain are now task local.
>>>
>>> - Binary Files:
>>>    As before the target platforms JavaScript
>>> nodeJS, Python and Java support file system
>>> access. A new open option type/1 has been added,
>>> which can have the values 'text' or 'binary' and
>>> which defaults to 'text'. 'binary' is simply
>>> treated as 'text' with latin1 encoding instead of utf8.
>>>
>>> - Binary HTTP:
>>>    To give the benefit of a simple binary
>>> treatment to the HTTP protocol as well, i.e. no
>>> extra get_byte/[1,2] builtins and no extra byte
>>> array datatype, since codes and atoms can be used
>>> as before, we braught the type/1 option to the
>>> APIs of the HTTP clients and the HTTP servers.
>>>
>>> Have Fun!
>>> Jan Burse, 22.05.2024, http://www.xlog.ch/
>>
> 

Back to comp.lang.java.programmer | Previous | Next | Find similar

Thread

Re: ANN: Dogelog Player 1.2.0 (Binary Streams) Mild Shock <janburse@fastmail.fm> - 2024-07-09 21:39 +0200

csiph-web