2
$\begingroup$

A inference system is a set of rules that can be used to prove something in some formal model. I understand that.

But what does it mean to a inference system to be local?

For instance, in the page 36 of these MPRI notes there is the following definition:

Definition 4.2 (locality) Let $I$ be an inference system. The system $I$ is local if whenever $T ⊢ u$ in $I$, there exists a proof $\Pi$ of $T ⊢ u$ such that $Steps(\Pi) \subset st(T \cup \{u\})$.

But I am not able to understand this definition because even if I know that $st(T\cup\{u\})$ is the set of subterms of $T \cup \{u\}$, I don't know what is $Steps(\Pi)$.

$\endgroup$
2
$\begingroup$

$\mathsf{Steps}(\Pi)$ is defined just above, in the paragraph below Definition 4.1. It's the set of node labels in the proof, i.e. the set of propositions that are proved as lemmas in that proof.

Thus a local inference system is a set of propositions such that every deduction $T \vdash u$ can be proved from lemmas that only involve terms that are subterms of the proposition $u$ or of the premises $T$.

$\endgroup$
  • $\begingroup$ So, in the tree presented in example 4.2, do we have $Steps(\Pi) = \{a, b, (a, b) \}$ ? $\endgroup$ – Hilder Vitor Lima Pereira Mar 9 '16 at 12:45
  • $\begingroup$ The labels are the conclusions of each node or the premises used in each node counts too ? $\endgroup$ – Hilder Vitor Lima Pereira Mar 9 '16 at 12:46
  • 1
    $\begingroup$ @Vitor The label is the conclusion, e.g. $u$. In Example 4.2, there's also $\textsf{senc}(s, \langle a, b \rangle)$ and so on. $\endgroup$ – Gilles 'SO- stop being evil' Mar 9 '16 at 13:30
  • $\begingroup$ Ok, the conclusions of each node. Got it. And the subterms of $T \cup \{u\}$ would be just $\{(senc(s,(a,b)), a), senc(b,a), s\}$ in this example? $\endgroup$ – Hilder Vitor Lima Pereira Mar 9 '16 at 13:36
  • 1
    $\begingroup$ @Vitor Also $a$, $b$ and $\langle a,b\rangle$. $\endgroup$ – Gilles 'SO- stop being evil' Mar 9 '16 at 13:38

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.