Abstract | ||
---|---|---|
A way is found to add axioms to sequent calculi that maintains the eliminability of cut, through the representation of axioms as rules of inference of a suitable form. By this method, the structural analysis of proofs is extended from pure logic to free-variable theories, covering all classical theories, and a wide class of constructive theories. All results are proved for systems in which also the rules of weakening and contraction can be eliminated. Applications include a system of predicate logic with equality in which also cuts on the equality axioms are eliminated. |
Year | DOI | Venue |
---|---|---|
1998 | 10.2307/420956 | BULLETIN OF SYMBOLIC LOGIC |
Keywords | Field | DocType |
structure analysis | Discrete mathematics,Axiom,Mathematics | Journal |
Volume | Issue | ISSN |
4 | 4 | 1079-8986 |
Citations | PageRank | References |
42 | 4.81 | 1 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Sara Negri | 1 | 280 | 24.76 |
Jan Von Plato | 2 | 194 | 29.54 |