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

# Untitled

By: a guest on May 1st, 2012  |  syntax: None  |  size: 0.89 KB  |  hits: 14  |  expires: Never
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.