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: Mon, 8 Jul 2024 07:32:29 +0200
Message-ID: <v6ftld$appo$1@solani.org>
References: <v2kb7s$kakr$1@solani.org> <v4t7nm$1rd2b$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 8 Jul 2024 05:32:29 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="354104"; 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:TgfEWQvYfVM0+CE041BCQd276L4=
X-User-ID: eJwNysEBwCAIA8CVCJCo44iV/Uew9z6GoDNSVLLZSltsNPeeHhVuuOxbGtXrOCvm+d/UzsgCv0LBbiwL0uEPR3wUvg==
In-Reply-To: <v4t7nm$1rd2b$1@solani.org>
Bytes: 3805
Lines: 81


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