[Attempto] question regarding Satchmo theorem prover

[Norbert E. Fuchs]

> On 13 May 2015, at 4:36 , Tiantian Gao <gao.tany at gmail.com> wrote:
> 
> Satchmo theorem prover is coded in Prolog. I am curious where I can get its open source code for Satchmo? BTW, which version of Satchmo RACE reasoner is based on to conduct reasoning?

Hi Tiantian Gao

I am the author of RACE.

Currently I am about to make RACE shipshape, i.e. cleaning the code, updating the documentation, and collecting and organising the many text cases, before I will submit it to GitHub with a GNU Lesser General Public License. 

I do not quite understand your question 

> which version of Satchmo RACE reasoner is based on to conduct reasoning?


Do you mean the version of Prolog in which RACE is coded? If yes, I am currently using the latest stable version of SWI Prolog, i.e. the Unix version 6.4.1, respectively the Mac application version 6.6.6. But RACE should run with most other versions of SWI Prolog. If you mean which version of the original Satchmo RACE is based on, I cannot give you a concrete answer. I based RACE many years ago on the following version of the original Satchmo

> satisfiable :-
>   setof(Clause, violated_instance(Clause), Clauses),
>   !,
>   satisfy_all(Clauses),
>   satisfiable.
> 
> satisfiable.
> 
> 
> violated_instance((satchmo_clause(B,H))) :-
>   satchmo_clause(B,H),
>   B,
>   \+ H.
>   
>   
> satisfy_all([]).
> 
> satisfy_all([(satchmo_clause(_B,H)) | RestClauses]) :-
>   H,
>   !,
>   satisfy_all(RestClauses).
> satisfy_all([satchmo_clause(_B,H) | RestClauses]) :-
>   satisfy(H),
>   satisfy_all(RestClauses).
> 
> /*
> satisfy((A,B)) :-
>   !,
>   satisfy(A),
>   satisfy(B).  
> */
> 
> satisfy((A;B)) :-
>   !,
>   (satisfy(A) ; satisfy(B)).  
>   
> satisfy(Atom) :-
>   \+ Atom = fail,
>   (
>     predicate_property(Atom, built_in)
>     ->
>     call(Atom)
>   ;
>     assume(Atom)
>   ).
> 
> 
> assume(Atom) :-
>   nl, write(['Asserting  ': Atom]),
>   asserta(Atom).
> 
> assume(Atom) :-
>   nl, write(['Retracting ': Atom]),
>   retract(Atom),
>   !,
>   fail.			

but have since strongly modified and expanded RACE's code – keeping only the basic idea of forward reasoning with clauses/rules – as you can see from the size of the respective programs. While the original Satchmo consists of some 20 lines, RACE consists of 9 modules with altogether 350k, not counting the ACE parsing engine APE that translates ACE axioms and theorems into the logic form of discourse representation structures.

Let me know if you have further questions. I am also interested to learn about your experience with the web-interface of RACE – which by the way is always up to date.

Regards.

Norbert E. Fuchs
Department of Informatics & Institute of Computational Linguistics
University of Zurich