@MSGID:
<69fe5f82-f386-4784-99fa-7c998be49093n@googlegroups.com> 20a3ea69
@REPLY: 1@solani.org> f9d7e9cc
@REPLYADDR Mild Shock <bursejan@gmail.com>
@REPLYTO 2:5075/128 Mild Shock
@CHRS: CP866 2
@RFC: 1 0
@RFC-References: 1@solani.org>
1@solani.org>
@RFC-Message-ID:
<69fe5f82-f386-4784-99fa-7c998be49093n@googlegroups.com>
@TZUTC: -0700
@PID: G2/1.0
@TID: FIDOGATE-5.12-ge4e8b94
We are currently investigating cartesian logic. To 
reduce the complexity of our endeavour we explored 
embedded implication as a means to provide a logic 
framework. We can show natural deduction and gentzen 
style proof search, as well as fitch proof rendering.

We use a proof renderer that is based the rule/2 clauses 
for natural deduction and not by the right/2 and left/4 
clauses for Gentzen style. Toying with our ~(A->B) = (A/\\~B) 
example, we find that Gentzen style, although still non-
deterministic, is 25-times faster than natural deduction.

See also:

Embedded Implication as a Logic Framework
https://twitter.com/dogelogch/status/1681326945701593088

Embedded Implication as a Logic Framework
https://www.facebook.com/groups/dogelog

Mostowski Collapse schrieb am Donnerstag, 6. Juli 2023 um 23:04:14 UTC+2:
> In this article we provide a sequel to our automated 
> first order theorem proover. The initial version 
> was only based on the implicational fragment of 
> first order logic. We changed the prover to also support 
> conjunction. 
> 
> The result is a new prover again written in Dogelog 
> Player, a Prolog system for the JavaScript and Python 
> platform. For the JavaScript platform, the prover can 
> be run in the browser completely client side. 
> 
> The exact same conjunction rules can be also added 
> to intuitionistic logic. Here in classical logic 
> conjunction is rather redundant, since we have the 
> dual ?(A ? B) = (A ? ?B). If we would further add 
> disjunction, we would end in bi-cartesian logic. 
> 
> See also: 
> 
> Cartesian Logic in Dogelog Player 
> https://twitter.com/dogelogch/status/1677059262734901254 
> 
> Cartesian Logic in Dogelog Player 
> https://www.facebook.com/groups/dogelog
> Mild Shock wrote: 
> > Dear All, 
> > 
> > We are happy to announce a new edition 
> > of the Dogelog player: 
> > 
> > - library(react): 
> >    The library(markup) library was rewritten 
> > and some new predicates were added. All 
> > predicates related to DOM events are now 
> > available in a new library library(react). 
> > Both libraries also include conveniences for SVG. 
> > 
> > - library(json): 
> >   The library(json) library, previously 
> > rolled out for Jekejeke Prolog, is also 
> > available for Dogelog Player. The library 
> > has now been extended slightly, so there 
> > is a predicate to convert JSON terms between 
> > atoms, and predicates to address JSON 
> > terms which are objects. 
> > 
> > - GNU Prolog Stub: 
> >   Libraries like library(json) can also be 
> > used from GNU Prolog if ensure loaded/1 is 
> > replaced with include/1. GNU Prolog results 
> > have been added to the benchmark and 
> > compliance testing suites. Perhaps it will 
> > soon be possible to compile Dogelog Player 
> > with GNU Prolog. 
> > 
> > Have Fun! 
> > Jan Burse, 18.06.2023, http://www.xlog.ch/
--- G2/1.0
 * Origin: usenet.network (2:5075/128)
SEEN-BY: 5001/100 5005/49 5015/255 5019/40 5020/715
848 1042 4441 12000
SEEN-BY: 5030/49 1081 5058/104 5075/128
@PATH: 5075/128 5020/1042 4441