The following pages link to (Q5813181):
Displaying 40 items.
- A constructive version of Tarski's geometry (Q490871) (← links)
- Forum: A multiple-conclusion specification logic (Q671512) (← links)
- Coherence in Cartesian closed categories and the generality of proofs (Q750442) (← links)
- Resolution is cut-free (Q972424) (← links)
- A proof-theoretic study of the correspondence of hybrid logic and classical logic (Q1006454) (← links)
- Coherence in linear predicate logic (Q1011758) (← links)
- A solver for QBFs in negation normal form (Q1020501) (← links)
- A propositional fragment of Leśniewski's ontology and its formulation by the tableau method (Q1078555) (← links)
- Solvable classes of pseudoprenex formulas (Q1147118) (← links)
- A new reduction sequence for arithmetic (Q1167719) (← links)
- A coherence theorem for canonical morphisms in Cartesian closed categories (Q1168319) (← links)
- Existential instantiation and normalization in sequent natural deduction (Q1198828) (← links)
- A specialization of the form of deductions in Gentzen calculi and its applications (Q1245933) (← links)
- Representing scope in intuitionistic deductions (Q1274448) (← links)
- Permutability of proofs in intuitionistic sequent calculi (Q1275625) (← links)
- Termination of permutative conversions in intuitionistic Gentzen calculi (Q1275632) (← links)
- Proof-functional connectives and realizability (Q1330311) (← links)
- Constant-only multiplicative linear logic is NP-complete (Q1342254) (← links)
- On the intuitionistic force of classical search (Q1575923) (← links)
- Correspondences between classical, intuitionistic and uniform provability (Q1575924) (← links)
- Brouwer and Euclid (Q1688971) (← links)
- Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
- Coherence for closed categories with biproducts (Q2200954) (← links)
- Theorem prover for intuitionistic logic based on the inverse method (Q2216868) (← links)
- Coherence in SMCCs and equivalences on derivations in IMML with unit (Q2373695) (← links)
- Elimination of cut-type rules from the Robinson and Presburger axiomatic systems (Q2557246) (← links)
- On the cut operation in Gentzen calculi (Q3236672) (← links)
- A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms (Q3540178) (← links)
- Axiom Directed Focusing (Q3638252) (← links)
- Semantical Completeness Theorems in Logic and Algebra (Q3900058) (← links)
- Three faces of natural deduction (Q4610312) (← links)
- On the intuitionistic force of classical search (Extended abstract) (Q4645244) (← links)
- A proof-theoretic study of the correspondence of classical logic and modal logic (Q4650293) (← links)
- Correct Answers for First Order Logic (Q4923518) (← links)
- Proof Transformations and Structural Invariance (Q5426006) (← links)
- Mechanising Gödel-Löb provability logic in HOL light (Q6050769) (← links)
- Upper and lower bounds for the height of proofs in sequent calculus for intuitionistic logic (Q6147867) (← links)
- Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory (Q6597957) (← links)
- Focusing Gentzen's LK proof system (Q6612872) (← links)
- Special cases of the interpolation theorem for classical predicate calculus (Q6647873) (← links)
