5
$\begingroup$

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

||cite|improve this question
$\endgroup$
  • 2
    $\begingroup$ What does it mean to "execute an inference rule"? Do you mean a proof search algorithm? $\endgroup$ – cody Mar 27 '16 at 14:47
  • $\begingroup$ Yes, I mean the proof search algorithm. I see that many CS papers just present inference rules without presenting any strategy to apply them $\endgroup$ – Trung Ta Mar 29 '16 at 7:42
  • $\begingroup$ The proof search algorithm is mostly independent from the proof system, which stands on its own. $\endgroup$ – Raphael♦ Mar 29 '16 at 17:42
  • 2
    $\begingroup$ We expect references to fulfill the minimal scholarly requirements and be as robust over time as possible. Please take some time to improve your post in this regard. We have collected some advice here. $\endgroup$ – Raphael♦ Mar 29 '16 at 17:43
8
$\begingroup$

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:

  1. Given $\Gamma\vdash\varphi$, is this sequent derivable?
  2. 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:

  1. What order do we apply rules in?
  2. 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.
  3. 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.

||cite|improve this answer
$\endgroup$
  • $\begingroup$ Thank you very much for your detailed answer! I want to clarify about your last opinion that "to separate the system of rules from the algorithm". Does it mean it is good enough to present only either the system of rules or the algorithm? Or should both of them be presented? $\endgroup$ – Trung Ta Mar 30 '16 at 2:32
  • 1
    $\begingroup$ @TrungTa in general, the rules are significantly clearer than the algorithm, and are much more amenable to proofs of meta-theoretical properties, e.g. consistency (the fact that not all things can be proven). In propositional logic for example, the usual algorithms for provability are quite complex (relying on backtracking), and even termination is non-trivial. So I'd say it's usually a good idea to present both algorithm and rules separately. $\endgroup$ – cody Mar 30 '16 at 14:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.