patternMinor
Why do presenttations of proof systems in logic and automated reasoning not include the algorithm that finds proofs?
Viewed 0 times
reasoningwhytheincludesystemslogicautomatedalgorithmpresenttationsthat
Problem
Is is that a common way to present a proof system in the field of Logic and Automated Reasoning is to present a system of inference rules, without having to formally describe a particular algorithm or procedure to find proofs in this system?
I notice that phenomenon in both textbook as well as conference or journal papers of this field.
This can be seen in classic topics like: the Natural Deduction calculus, Hilbert calculus where only inference rules is presented.
In modern researches, I am studying about Separation Logic, thus, I would like to take some papers from this field to illustrate this observation:
Automated Cyclic Entailment Proofs in Separation Logic
Symbolic Execution with Separation Logic
I notice that phenomenon in both textbook as well as conference or journal papers of this field.
This can be seen in classic topics like: the Natural Deduction calculus, Hilbert calculus where only inference rules is presented.
In modern researches, I am studying about Separation Logic, thus, I would like to take some papers from this field to illustrate this observation:
Automated Cyclic Entailment Proofs in Separation Logic
Symbolic Execution with Separation Logic
Solution
To simplify a bit, a system of inference rules generally defines a set of sequents, which are simply pairs of a list (or set) of propositions $\Gamma$ and a proposition $\phi$ written
$$ \Gamma \vdash \varphi$$
called the derivable sequents. The rules describe which sequents are derivable, and for any reasonable system, given $\Gamma\vdash\varphi$, and sequents $\Gamma_1\vdash\varphi_1,\ldots,\Gamma_n\vdash\varphi_n$, it is easy to tell whether
$$\frac{\Gamma_1\vdash\varphi_1\ldots \Gamma_n\vdash\varphi_n}{\Gamma\vdash\varphi} $$
is a valid derivation. This usually be done with some obvious algorithm.
Some much more difficult algorithmic questions are this:
In general, there is no algorithm for answering question 1, and question 2 is quite difficult. In particular, when trying to prove $\Gamma\vdash\varphi$ a natural approach is to try to apply all possible rules until exhaustion. Several issues come up:
Because of the complexity of these issues, it's much more natural to separate the system of rules that describe the derivable sequents from the algorithms trying to find actual derivations of a given sequent.
$$ \Gamma \vdash \varphi$$
called the derivable sequents. The rules describe which sequents are derivable, and for any reasonable system, given $\Gamma\vdash\varphi$, and sequents $\Gamma_1\vdash\varphi_1,\ldots,\Gamma_n\vdash\varphi_n$, it is easy to tell whether
$$\frac{\Gamma_1\vdash\varphi_1\ldots \Gamma_n\vdash\varphi_n}{\Gamma\vdash\varphi} $$
is a valid derivation. This usually be done with some obvious algorithm.
Some much more difficult algorithmic questions are this:
- Given $\Gamma\vdash\varphi$, is this sequent derivable?
- Given $\Gamma$, how can we enumerate the set of $\varphi$ such that $\Gamma\vdash \varphi$ is derivable?
In general, there is no algorithm for answering question 1, and question 2 is quite difficult. In particular, when trying to prove $\Gamma\vdash\varphi$ a natural approach is to try to apply all possible rules until exhaustion. Several issues come up:
- What order do we apply rules in?
- How do we guess the $\Gamma_i\vdash \varphi_i$? If any variables appear on top that do not appear in the conclusion, you need to guess some instance for that variable.
- When do we know if a derivation does not exist?
Because of the complexity of these issues, it's much more natural to separate the system of rules that describe the derivable sequents from the algorithms trying to find actual derivations of a given sequent.
Context
StackExchange Computer Science Q#54992, answer score: 8
Revisions (0)
No revisions yet.