A compact representation of proofs
From MaRDI portal
Publication:1102282
DOI10.1007/BF00370646zbMath0644.03033OpenAlexW2084443499MaRDI QIDQ1102282
Publication date: 1987
Published in: Studia Logica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00370646
sequent calculusSkolem functionsproof treesexpansion treesHerbrand universeautomatically generated proofsfirst-order interpolation theoremfragment of simple type theorylinear proofs
Related Items
On the complexity of proof deskolemization, Nominal logic, a first order theory of names and binding, Proof generalization in \(\mathrm {LK}\) by second order unifier minimization, TPS: A hybrid automatic-interactive system for developing proofs, TPS: A theorem-proving system for classical type theory, Direct deductive computation on discourse representation structures, Unnamed Item, On the Herbrand content of LK, A realizability interpretation of Church's simple theory of types, First-order interpolation derived from propositional interpolation, A semantic framework for proof evidence, Classical proof forestry, On connections and higher-order logic, Analytic tableaux for higher-order logic with choice, Unnamed Item, On the elimination of quantifier-free cuts, Combining and automating classical and non-classical logics in classical higher-order logics, Extraction of expansion trees, Herbrand's theorem as higher order recursion, Optimized encodings of fragments of type theory in first order logic, Unnamed Item, On the form of witness terms, CERES in higher-order logic, Progress in the Development of Automated Theorem Proving for Higher-Order Logic, Unnamed Item, A Clausal Approach to Proof Analysis in Second-Order Logic, System Description: GAPT 2.0, Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic, GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION, Expansion trees with cut, Deep inference and expansion trees for second-order multiplicative linear logic, Mechanized metatheory revisited, Induction and Skolemization in saturation theorem proving, A combinator-based superposition calculus for higher-order logic
Cites Work
- A proof of cut-elimination theorem in simple type-theory
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Hauptsatz for higher order logic
- Resolution in type theory
- A Complete Mechanization of Second-Order Type Theory
- A formulation of the simple theory of types
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
