A compact representation of proofs
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 3871341 (Why is no real title available?)
- scientific article; zbMATH DE number 3878393 (Why is no real title available?)
- scientific article; zbMATH DE number 3275554 (Why is no real title available?)
- scientific article; zbMATH DE number 3274715 (Why is no real title available?)
- scientific article; zbMATH DE number 3362981 (Why is no real title available?)
- A Complete Mechanization of Second-Order Type Theory
- A formulation of the simple theory of types
- A proof of cut-elimination theorem in simple type-theory
- Hauptsatz for higher order logic
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Resolution in type theory
Cited in
(39)- Herbrand's theorem as higher order recursion
- scientific article; zbMATH DE number 7447752 (Why is no real title available?)
- 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
- scientific article; zbMATH DE number 3871341 (Why is no real title available?)
- Game semantics and the geometry of backtracking: a new complexity analysis of interaction
- Mechanized metatheory revisited
- On the form of witness terms
- scientific article; zbMATH DE number 7350767 (Why is no real title available?)
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic
- The TPS theorem proving system
- Combining and automating classical and non-classical logics in classical higher-order logics
- A combinator-based superposition calculus for higher-order logic
- Optimized encodings of fragments of type theory in first order logic
- On connections and higher-order logic
- Nominal logic, a first order theory of names and binding
- Presenting intuitive deductions via symmetric simplification
- 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
- Accelerating tableaux proofs using compact representations
- Classical proof forestry
- scientific article; zbMATH DE number 7559288 (Why is no real title available?)
- TPS: A hybrid automatic-interactive system for developing proofs
- scientific article; zbMATH DE number 7533330 (Why is no real title available?)
- On the elimination of quantifier-free cuts
- First-order interpolation derived from propositional interpolation
- Expansion trees with cut
- A semantic framework for proof evidence
- A Clausal Approach to Proof Analysis in Second-Order Logic
- Extraction of expansion trees
- Induction and Skolemization in saturation theorem proving
- Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic
- 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)
