How to compute the consequence set of the set of premises for for first order logic? I.e. how to compute the right hand side of the judgment given the left hand side. Of course, there are 3 kind of sequent calculus of the FOL and that act upon judgments but there are relatively few sequent rules that leave the left hand side (set of premises) untouched, there are sequent rules that from judgment deduced different judgment with completely different left hand side (set of premises).

So - how to compute consequence set (part of it, of course, possibly - focused part of it) of the judgment? What type of software tools (solver, reasoner, proof assistant, theorem prover, sat/smt solver, etc.) can be used for this type of task?


1 Answer 1


In general, once you have proven a set of things $Q_1,\dots,Q_n$ from a set of premises $P_1,\dots,P_n$, you can conclude $P_1,\dots,P_n\vdash Q_1,\dots,Q_n$. This is true even when you have manipulated the terms so everything is on the RHS of the $\vdash$, as it appears in the sequent calculus.

To compute a focused part of the consequence set, you can use a process known as answer extraction. Here, a question is put to a database, in the form of $P(x)\rightarrow goal(x)$. For instance, if the database is the set of premises {f(art, jon),f(bob, kim),~f(x, y),p(x, y)}, you can ask the question: Who is Jon's parent?

\begin{align} 1.~&\{f(art, jon)\}&~\text{Premises}\\ 2.~&\{f(bob, kim)\}&~\text{Premises}\\ 3.~&\{\lnot f(x, y), p(x, y)\}&~\text{Premises}\\ 4.~&\{\lnot p(x, jon), goal(x)\}&~\text{Goal}\\ 5.~&\{\lnot f(x, jon), goal(x)\}&~3,4\\ 6.~&\{goal(art)\}&~1,5 \end{align}

Entries in the database must be in clausal form, for which automated conversion methods exist. The answer to the question is determined using a method known as resolution, which has just one deductive rule which is sound and complete and easily automated.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .