A compact representation of proofs
From MaRDI portal
DOI10.1007/BF00370646zbMATH Open0644.03033OpenAlexW2084443499MaRDI QIDQ1102282FDOQ1102282
Authors: Dale Miller 
Publication date: 1987
Published in: Studia Logica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00370646
Recommendations
sequent calculusSkolem functionsproof treesexpansion treesHerbrand universeautomatically generated proofsfirst-order interpolation theoremfragment of simple type theorylinear proofs
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- A formulation of the simple theory of types
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Resolution in type theory
- Hauptsatz for higher order logic
- A proof of cut-elimination theorem in simple type-theory
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Complete Mechanization of Second-Order Type Theory
- Title not available (Why is that?)
Cited In (39)
- Title not available (Why is that?)
- Herbrand's theorem as higher order recursion
- Direct deductive computation on discourse representation structures
- A realizability interpretation of Church's simple theory of types
- Deep inference and expansion trees for second-order multiplicative linear logic
- On the Herbrand content of LK
- Title not available (Why is that?)
- Game semantics and the geometry of backtracking: a new complexity analysis of interaction
- Title not available (Why is that?)
- Mechanized metatheory revisited
- On the form of witness terms
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- The TPS theorem proving system
- Optimized encodings of fragments of type theory in first order logic
- A combinator-based superposition calculus for higher-order logic
- Combining and automating classical and non-classical logics in classical higher-order logics
- Presenting intuitive deductions via symmetric simplification
- Nominal logic, a first order theory of names and binding
- On connections and higher-order logic
- Focusing Gentzen's LK proof system
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization
- Analytic tableaux for higher-order logic with choice
- On the complexity of proof deskolemization
- TPS: A theorem-proving system for classical type theory
- Title not available (Why is that?)
- Accelerating tableaux proofs using compact representations
- Classical proof forestry
- TPS: A hybrid automatic-interactive system for developing proofs
- Title not available (Why is that?)
- On the elimination of quantifier-free cuts
- First-order interpolation derived from propositional interpolation
- Expansion trees with cut
- A Clausal Approach to Proof Analysis in Second-Order Logic
- A semantic framework for proof evidence
- Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic
- Induction and Skolemization in saturation theorem proving
- Extraction of expansion trees
- CERES in higher-order logic
- System description: GAPT 2.0
This page was built for publication: A compact representation of proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1102282)
