Many interesting problems can be presented declaratively using predicate logic. Real life examples are scheduling, logistics, and software and electric circuit verification. That is, the problems are hard and logic provides a way to solve them declaratively. Logic solvers take as input the problem declaration and spit out the solution to the problem.

Examples of solvers are the famous Z3 and GKC. Z3 uses SMTLIB language to specify the problem. GKC is from a different family, and uses TPTP language. The languages are quite different and it seems to me that SMT is geared towards propositional logic while TPTP is for predicate logic. I couldn’t find any simple comparison so I made one.

Our toy predicate logic problem is as follows. We have four people: Agnetha, Björn, Benny, and Anni-Frid (“Frida”), and one binary predicate knows(x,y). We know a priori that:

• knows(Agnetha, Björn), that is, Agnetha knows Björn.
• knows(Benny, Björn)
• ∀x∀y(knows(x,y)→knows(y,x))
• ∀y¬knows(Frida,y)

Can we say for sure that Agnetha doesn’t know Frida? That is, does the logical consequence hold: S ⊨ ¬knows(Agnetha,Frida)? Simple, but how to write the structure in SMTLIB and TPTP?

First TPTP. The syntax fits this kind of problem very nicely and is clear. Runnning: bin/gkc ./abba.tptp

fof(formula1,axiom, (knows(agnetha,bjorn))).
fof(formula2,axiom, (knows(benny,bjorn))).
fof(formula3,axiom, (! [X] : ! [Y] : ((~ knows(X,Y)) | knows(Y,X)))).
fof(formula4,axiom, (! [X] : ~ knows(frida, X))).
% Proof by contradiction
fof(formula5,conjecture, (~ knows(agnetha,frida))).

Next, the same in SMTLIB. Run with bin/z3 -smt2 abba.smt

; https://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf
;(set-logic AUFLIA)
(declare-sort A 0) ; A new sort for persons
(declare-fun knows (A A) Bool)
(declare-const agnetha A)
(declare-const bjorn A)
(declare-const benny A)
(declare-const frida A)
(assert (knows agnetha bjorn))
(assert (knows benny bjorn))
(assert (forall ((x A) (y A)) (=> (knows x y) (knows y x))))
(assert (forall ((x A)) (not (knows frida x))))
;(check-sat)
;(get-model)
; assert the negation of the conjecture
(assert(knows agnetha frida))
(check-sat)

There we have it, the same problem solved in both TPTP and SMTLIB.

This is interesting because the solvers are getting really capable nowadays. Geoff Sutcliffe has written a nice piece about Automated Theorem Proving and how it can be utilized to solve age-old problems.

ATP is thus a technology very suited to situations where a clear thinking domain expert can interact with a powerful tool, to solve interesting and deep problems.

Geoff Sutcliffe