Don't like ads? PRO users don't see any ads ;-)
Public Pastes
Guest

Untitled

By: a guest on May 1st, 2012  |  syntax: None  |  size: 0.89 KB  |  hits: 14  |  expires: Never
download  |  raw  |  embed  |  report abuse  |  print
Text below is selected. Please press Ctrl+C to copy to your clipboard. (⌘+C on Mac)
  1. Has anybody seen a good open source Prolog implementation of the SATCHMO theorem prover?
  2. :- op(1200, xfx, '--->').
  3. :- unknown(_, fail).
  4.  
  5. satisfiable :-
  6.   setof(Clause, violated_instance(Clause), Clauses),
  7.   !,
  8.   satisfy_all(Clauses),
  9.   satisfiable.
  10. satisfiable.
  11.  
  12. violated_instance((B ---> H)) :-
  13.   (B ---> H),
  14.   B,
  15.   + H.
  16.  
  17. satisfy_all([]).
  18.  
  19. satisfy_all([(_B ---> H) | RestClauses]) :-
  20.   H,
  21.   !,
  22.   satisfy_all(RestClauses).
  23. satisfy_all([(_B ---> H) | RestClauses]) :-
  24.   satisfy(H),
  25.   satisfy_all(RestClauses).
  26.  
  27. /*
  28. satisfy((A,B)) :-
  29.   !,
  30.   satisfy(A),
  31.   satisfy(B).  
  32. */
  33.  
  34. satisfy((A;B)) :-
  35.   !,
  36.   (satisfy(A) ; satisfy(B)).  
  37.  
  38. satisfy(Atom) :-
  39.   + Atom = untrue,
  40.   (
  41.     predicate_property(Atom, built_in)
  42.     ->
  43.     call(Atom)
  44.   ;
  45.     assume(Atom)
  46.   ).
  47.  
  48. assume(Atom) :-
  49. %  nl, write(['Asserting  ': Atom]),
  50.   asserta(Atom).
  51.  
  52. assume(Atom) :-
  53. %  nl, write(['Retracting ': Atom]),
  54.   retract(Atom),
  55.   !,
  56.   fail.
create a new version of this paste RAW Paste Data