# How to compute the consequence set of the set of premises for for first order logic?

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?

• Do you have a specific task in mind? Commented Nov 2, 2019 at 20:45
• After you ask a question here, if you get an acceptable answer, you should "accept" the answer by clicking the check mark $\checkmark$ next to it. This scores points for you and for the person who answered your question. You can find out more about accepting answers here: How do I accept an answer?, Why should we accept answers?, What should I do if someone answers my question?. Commented May 30, 2020 at 10:06

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}