Satchmo source? 
Author Message
 Satchmo source?

Anybody seen some downloadable source for the theorem prover Satchmo or
Satchmore, or some other Prolog based theorem prover?

thx



Fri, 10 Jun 2005 21:41:28 GMT  
 Satchmo source?


Quote:
> Anybody seen some downloadable source for the theorem prover Satchmo or
> Satchmore, or some other Prolog based theorem prover?

> thx

Here is one version of Satchmo. Google gives you more on Satchmo and on
Satchmore.

:- op(1200, xfx, '--->').
:- unknown(_, fail).

satisfiable :-
  setof(Clause, violated_instance(Clause), Clauses),
  !,
  satisfy_all(Clauses),
  satisfiable.
satisfiable.

violated_instance((B ---> H)) :-
  (B ---> H),
  B,
  \+ H.

satisfy_all([]).
satisfy_all([(_B ---> H) | RestClauses]) :-
  H,
  !,
  satisfy_all(RestClauses).
satisfy_all([(_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 = false,
  (
    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.

Norbert E. Fuchs
Institut fr Informatik
Universit?t Zrich



Sat, 25 Jun 2005 05:02:08 GMT  
 
 [ 2 post ] 

 Relevant Pages 

1. APL2C source to source adapter?

2. The source and the sink different type with its source code

3. REFILL, SOURCE and SOURCE-ID current practice?

4. Metacompile assembly source to assembly source ?

5. Find Forth source (was: 8031 Forth Source Code Needed)

6. Source->Source Transformations in Haskell

7. source-to-source translators

8. Translating in source that is to be inlined into other source

9. Source Code Formatter - with source

10. Data Recovery SOURCE CODE ( SOURCE CODES of Professional Data Recovery Software )

11. Wanted: Pascal/Ada source analyzer (was Re: WANTED: C source analyser)

12. Converting FORTRAN source code to C source code

 

 
Powered by phpBB® Forum Software