[Attempto] question regarding Satchmo theorem prover

[Tany Gao]

Thank you, Professor Fuchs, for such detailed explanation. It helps me a
lot.

-- Tany

On Wed, May 13, 2015 at 6:24 AM, Norbert E. Fuchs <fuchs at ifi.uzh.ch> wrote:

>
> > 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
>
>
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.ifi.uzh.ch/pipermail/attempto/attachments/20150513/8cfa12c1/attachment.html>