Name
Abstract | ||
|---|---|---|
A formulation of lattice theory as a system of rules added to sequent calculus is given. The analysis of proofs for the contraction-free calculus of classical predicate logic known as G3c extends to derivations with the mathematical rules of lattice theory. It is shown that minimal derivations of quantifier-free sequents enjoy a subterm property: all terms in such derivations are terms in the endsequent.An alternative formulation of lattice theory as a system of rules in natural deduction style is given, both with explicit meet and join constructions and as a relational theory with existence axioms. A subterm property for the latter extends the standard decidable classes of quantificational formulas of pure predicate calculus to lattice theory. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1017/S0960129504004244 | Mathematical Structures in Computer Science |
Keywords | Field | DocType |
contraction-free calculus,lattice theory,classical predicate logic,alternative formulation,subterm property,minimal derivation,relational theory,existence axiom,pure predicate calculus,proof system,mathematical rule | Discrete mathematics,Lattice (order),Sequent calculus,Mathematical proof,Predicate logic,Mathematics,Calculus | Journal |
Volume | Issue | ISSN |
14 | 4 | 0960-1295 |
Citations | PageRank | References |
10 | 1.16 | 4 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Sara Negri | 1 | 280 | 24.76 |
| Jan Von Plato | 2 | 194 | 29.54 |