Pages that link to "Item:Q1102282"
From MaRDI portal
The following pages link to A compact representation of proofs (Q1102282):
Displaying 34 items.
- Proof generalization in \(\mathrm {LK}\) by second order unifier minimization (Q331619) (← links)
- Analytic tableaux for higher-order logic with choice (Q438561) (← links)
- Classical proof forestry (Q636369) (← links)
- On the elimination of quantifier-free cuts (Q650922) (← links)
- Combining and automating classical and non-classical logics in classical higher-order logics (Q656826) (← links)
- Extraction of expansion trees (Q670704) (← links)
- CERES in higher-order logic (Q716500) (← links)
- TPS: A hybrid automatic-interactive system for developing proofs (Q865629) (← links)
- On connections and higher-order logic (Q908896) (← links)
- On the form of witness terms (Q982183) (← links)
- A semantic framework for proof evidence (Q1701039) (← links)
- Nominal logic, a first order theory of names and binding (Q1887151) (← links)
- TPS: A theorem-proving system for classical type theory (Q1923825) (← links)
- Herbrand's theorem as higher order recursion (Q1987218) (← links)
- Induction and Skolemization in saturation theorem proving (Q2084957) (← links)
- A combinator-based superposition calculus for higher-order logic (Q2096452) (← links)
- First-order interpolation derived from propositional interpolation (Q2193292) (← links)
- Mechanized metatheory revisited (Q2323447) (← links)
- System Description: GAPT 2.0 (Q2817928) (← links)
- On the complexity of proof deskolemization (Q2892685) (← links)
- (Q3384900) (← links)
- A Clausal Approach to Proof Analysis in Second-Order Logic (Q3605531) (← links)
- Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic (Q3637204) (← links)
- Direct deductive computation on discourse representation structures (Q4312345) (← links)
- A realizability interpretation of Church's simple theory of types (Q4593235) (← links)
- Optimized encodings of fragments of type theory in first order logic (Q4647585) (← links)
- GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION (Q4977225) (← links)
- (Q4989394) (← links)
- On the Herbrand content of LK (Q5015361) (← links)
- (Q5079725) (← links)
- (Q5089024) (← links)
- Progress in the Development of Automated Theorem Proving for Higher-Order Logic (Q5191100) (← links)
- Expansion trees with cut (Q5236547) (← links)
- Deep inference and expansion trees for second-order multiplicative linear logic (Q5236548) (← links)
