Path: ...!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: comp.lang.prolog
Subject: Re: ANN: Dogelog Player 1.2.0 (Binary Streams)
Date: Tue, 9 Jul 2024 21:38:43 +0200
Message-ID: <v6k3k3$dpk7$1@solani.org>
References: <v2kb7s$kakr$1@solani.org> <v4t7nm$1rd2b$1@solani.org>
 <v6ftld$appo$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 9 Jul 2024 19:38:43 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="452231"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.18.2
Cancel-Lock: sha1:bmkslUiyC5tOZYiyHGOje8wVgM4=
X-User-ID: eJwFwQkBACAIA8BKfBsaBxT7R/AOTuXJIBh4eJ4lbxrtlq6OiRNtBo7pYUuh5EIa2KNkzjLfHFmYu3bJBz/1FMY=
In-Reply-To: <v6ftld$appo$1@solani.org>
Bytes: 4660
Lines: 105


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/
>>
>