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)$.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
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$.

Improve this answer
$\endgroup$
6
  • $\begingroup$ So, in the tree presented in example 4.2, do we have $Steps(\Pi) = \{a, b, (a, b) \}$ ? $\endgroup$
    – Hilder Vitor Lima Pereira
    Commented Mar 9, 2016 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
    Commented Mar 9, 2016 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'
    Commented Mar 9, 2016 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
    Commented Mar 9, 2016 at 13:36
  • 1
    $\begingroup$ @Vitor Also $a$, $b$ and $\langle a,b\rangle$. $\endgroup$
    – Gilles 'SO- stop being evil'
    Commented Mar 9, 2016 at 13:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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