Examples
To input proofs and try our method on them, you should use the proof input format described below and load .lks files using the program ProofTool. So far you can extract only the characteristic clause term, the characteristic clause set and the projection term schemata from the proof schema. Also there is possibility to evaluate proof schema to some number n and then apply the CERES method for classical LK.
You can find some of our test examples below (like The Adder Proof).
The Proof Input Format
The proof input format is designed to write LKS-proofs in a machine readable form using ASCII characters. An input proof can be written in any text editor, but should be saved as a plain text file with .lks extension. Below we briefly describe the syntax of this format assuming user has an LKS-proof already given. Description of the LKS calculus with full formal description of grammar of the proof input language, called HLKS, can be found here.
Atomic formulas, or indexed predicates, are written in first-order logic notation, predicate_name(index_1, . . . , index_n), where indices are linear arithmetic expressions, written as variable_name, number or variable_name + number. Then formulas are built using the following patterns:
~ formula,
(formula_1 / \ formula_2),
(formula_1 \ / formula_2),
BigAnd(variable_name = number .. arithmetic_expression) formula,
BigOr(variable_name = number .. arithmetic_expression) formula.
Finally, sequents are written as: formula_1, . . . , formula_n |- formula_n+1, . . . , formula_m.
One .lks file should contain at least one proof definition, which has the following pattern:
proof name proves sequent
base {
id_1 : rule_1
. . .
id_n : rule_n
root : rule_n+1
}
step {
id_1 : rule_1
. . .
id_m : rule_m
root : rule_m+1
}
where ids are any labels that are unique within { . . . } blocks (i.e. same labels can be used in the definition of base and step cases) and rules are patterns of the form:
| ax(sequent) | for an axiom sequent. | ||
| pLink((proof_name, arithmetic_expression) sequent) | for a proof link, which refers to the proof proof_name of the sequent sequent at the iteration arithmetic_expression. | ||
| rule_name(id, formula) | for unary rules with one auxiliary formula. | ||
| rule_name(id, formula_1, formula_2) | for unary rules with two auxiliary formulas. | ||
| rule_name(id_1, id_2, formula) | for binary rule(s) with one auxiliary formula. | ||
| rule_name(id_1, id_2, formula_1, formula_2) | for binary rules with two auxiliary formulas. |
where rule_name is defined according to the following table (the arity of rule_name depends on the corresponding LKS inference).
| rule_name | inference | rule_name | inference | |
|---|---|---|---|---|
| negL | \neg \colon l | andEqR1 | quiv \colon \land 1 | |
| negR | \neg \colon r | andEqR2 | quiv \colon \land 2 | |
| andR | \land \colon r | andEqR3 | quiv \colon \land 3 | |
| andL1 | \land \colon l1 | andEqL1 | quiv \colon \land 1 | |
| andL2 | \land \colon l2 | andEqL2 | quiv \colon \land 2 | |
| andL | shortcut for \land \colon l1, \land \colon l2, c \colon l | andEqL3 | quiv \colon \land 3 | |
| orL | \lor \colon l | orEqR1 | quiv \colon \lor 1 | |
| orR1 | \lor \colon r1 | orEqR2 | quiv \colon \lor 2 | |
| orR2 | \lor \colon r2 | orEqR3 | quiv \colon \lor 3 | |
| orR | shortcut for \lor \colon r1, \lor \colon r2, c \colon r | orEqL1 | quiv \colon \lor 1 | |
| cut | cut | orEqL2 | quiv \colon \lor 2 | |
| weakL | w \colon l | orEqL3 | quiv \colon \lor 3 | |
| weakR | w \colon r | |||
| contrL | c \colon l | |||
| contrR | c \colon r | |||
For example, the proof schema \psi of a sequent \vdash \bigwedge_{i=0}^{n} A_i, \bigvee_{i=0}^{n} \neg A_i is the following:
proof \psi proves |- BigAnd(i=0..n) A(i), BigOr(i=0..n) ~ A(i)
base {
1: ax(A(0) |- A(0))
2: negR(1, A(0))
3: orEqR3(2, ~ A(0), BigOr(i=0..0) ~ A(i))
root: andEqR3(3, A(0), BigAnd(i=0..0) A(i))
}
step {
1: pLink((\psi, n) |- BigAnd(i=0..n) A(i), BigOr(i=0..n) ~ A(i))
2: ax(A(n+1) |- A(n+1))
3: negR(2, A(n+1))
4: andR(1, 3, BigAnd(i=0..n) A(i), A(n+1))
5: orR(4, BigOr(i=0..n) ~ A(i), ~ A(n+1))
6: andEqR1(5, (BigAnd(i=0..n) A(i) /\ A(n+1)), BigAnd(i=0..n+1) A(i))
root: orEqR1(6, (BigOr(i=0..n) ~ A(i) \/ ~ A(n+1)), BigOr(i=0..n+1) ~ A(i))
}
The Adder Proof
We formalize proof of the theorem that a circuit n-bit adder is commutative. We use the lemma that the carry bits are equal. Introducing the following notations:
| A \oplus B | =_{def} | (A \land \neg B) \lor (\neg A \land B) |
| A \Leftrightarrow B | =_{def} | (\neg A \lor B) \land (\neg B \lor A) |
| Sum_i | =_{def} | S_i \Leftrightarrow (A_i \oplus B_i) \oplus C_i |
| Sum'_i | =_{def} | S'_i \Leftrightarrow (B_i \oplus A_i) \oplus C'_i |
| Carry_i | =_{def} | C_{i+1} \Leftrightarrow (A_i \land B_i) \lor (C_i \land A_i) \lor (C_i \land B_i) |
| Carry'_i | =_{def} | C'_{i+1} \Leftrightarrow (B_i \land A_i) \lor (C'_i \land B_i) \lor (C'_i \land A_i) |
| Adder_n | =_{def} | \bigwedge_{i=0}^n Sum_i \land \bigwedge_{i=0}^n Carry_i \land \neg C_0 |
| Adder'_n | =_{def} | \bigwedge_{i=0}^n Sum'_i \land \bigwedge_{i=0}^n Carry'_i \land \neg C'_0 |
| EqC_n | =_{def} | \bigwedge_{i=0}^n (C_i \Leftrightarrow C'_i) |
| EqC_n | =_{def} | \bigwedge_{i=0}^n (C_i \Leftrightarrow C'_i) |
| EqS_n | =_{def} | \bigwedge_{i=0}^n (S_i \Leftrightarrow S'_i) |
we prove
Adder_n, Adder'_n \vdash EqS_n
using cut on
\neg C_0, \neg C'_0, \bigwedge_{i=0}^n Carry_i, \bigwedge_{i=0}^n Carry'_i \vdash EqC_n and EqC_n, \bigwedge_{i=0}^n Sum_i, \bigwedge_{i=0}^n Sum'_i \vdash EqS_n
where
\neg C_0, \neg C'_0, \bigwedge_{i=0}^n Carry_i, \bigwedge_{i=0}^n Carry'_i \vdash EqC_n
is proved using the recursive cut on
\neg C_0, \neg C'_0, \bigwedge_{i=0}^n Carry_i, \bigwedge_{i=0}^n Carry'_i \vdash C_{n+1} \Leftrightarrow C'_{n+1} and C_{n+1} \Leftrightarrow C'_{n+1}, Carry_{n+1}, Carry'_{n+1} \vdash C_{n+2} \Leftrightarrow C'_{n+2}.
You can find fully formalized proof, typed using the proof input format described above, in adder.lks file and load it with ProofTool. Take into account that since the proof is big enough, if you want to apply some of our algorithms to the proof, you need to set some flags of java to enlarge the stack and heap sizes. For example, we use the following command:
> java -Xss20m -Xmx2g -jar prooftool.jar adder.lks
Now, we give rewrite rules and then characteristic clause terms of the adder proof. We have four cut-configurations, one for each LKS proof. Cut-configurations are written between parentheses and | is used as a separator between formulas from the antecedent and succeedent of the sequent. So, we have the following rewriting rules:
- cl_{0}^{(|), \psi} \rightarrow \Theta(\psi_{base}, (|))
- cl_{0}^{(|\bigwedge_{i=0}^n (C_i \Leftrightarrow C'_i)), \varphi} \rightarrow \Theta(\varphi_{base}, (|\bigwedge_{i=0}^n (C_i \Leftrightarrow C'_i)))
- cl_{0}^{(|C_{k+1} \Leftrightarrow C'_{k+1}), \phi} \rightarrow \Theta(\phi_{base}, (|C_{k+1} \Leftrightarrow C'_{k+1}))
- cl_{0}^{(\bigwedge_{i=0}^n (C_i \Leftrightarrow C'_i)|), \chi} \rightarrow \Theta(\chi_{base}, (\bigwedge_{i=0}^n (C_i \Leftrightarrow C'_i)|))
- cl_{k+1}^{(|), \psi} \rightarrow \Theta(\psi_{step}, (|))
- cl_{k+1}^{(|\bigwedge_{i=0}^n (C_i \Leftrightarrow C'_i)), \varphi} \rightarrow \Theta(\varphi_{step}, (|\bigwedge_{i=0}^n (C_i \Leftrightarrow C'_i)))
- cl_{k+1}^{(|C_{k+1} \Leftrightarrow C'_{k+1}), \phi} \rightarrow \Theta(\phi_{step}, (|C_{k+1} \Leftrightarrow C'_{k+1}))
- cl_{k+1}^{(\bigwedge_{i=0}^n (C_i \Leftrightarrow C'_i)|), \chi} \rightarrow \Theta(\chi_{step}, (\bigwedge_{i=0}^n (C_i \Leftrightarrow C'_i)|))
Now, we give characteristic clause terms of the adder proof. Notations are the following: negated cl variables, at the top of the terms, are giving information about these terms, i.e. for which proof and which cut-configuration they are computed. In fact, the first \otimes corresponds to the rewrite rule definition.
Characteristic clause terms for the base cases:
Characteristic clause terms for the step cases:
Projection terms for the base cases:
Projection terms for the step cases:
All these terms were obtained via ProofTool. If you are interested, please run the program and extract them using the menu items LKS Proof > Compute struct or LKS Proof > Compute Projection Term.