scientific article; zbMATH DE number 3074068

Cited in

(44)

A proof-theoretic study of the correspondence of hybrid logic and classical logic
Coherence in linear predicate logic
A solver for QBFs in negation normal form
A propositional fragment of Leśniewski's ontology and its formulation by the tableau method
Solvable classes of pseudoprenex formulas
A new reduction sequence for arithmetic
A coherence theorem for canonical morphisms in Cartesian closed categories
Existential instantiation and normalization in sequent natural deduction
A specialization of the form of deductions in Gentzen calculi and its applications
Representing scope in intuitionistic deductions
Permutability of proofs in intuitionistic sequent calculi
Termination of permutative conversions in intuitionistic Gentzen calculi
Proof-functional connectives and realizability
Constant-only multiplicative linear logic is NP-complete
On the intuitionistic force of classical search
Correspondences between classical, intuitionistic and uniform provability
Brouwer and Euclid
Theorem proving as constraint solving with coherent logic
Coherence for closed categories with biproducts
Theorem prover for intuitionistic logic based on the inverse method
Coherence in SMCCs and equivalences on derivations in IMML with unit
Elimination of cut-type rules from the Robinson and Presburger axiomatic systems
On the cut operation in Gentzen calculi
A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms
Axiom Directed Focusing
Semantical Completeness Theorems in Logic and Algebra
Three faces of natural deduction
On the intuitionistic force of classical search (extended abstract)
A proof-theoretic study of the correspondence of classical logic and modal logic
A constructive version of Tarski's geometry
Correct answers for first order logic
Proof Transformations and Structural Invariance
Mechanising Gödel-Löb provability logic in HOL light
Upper and lower bounds for the height of proofs in sequent calculus for intuitionistic logic
Investigations into proof-search in a system of first-order dependent function types
Synthesizing nested relational queries from implicit specifications: via model theory and via proof theory
Focusing Gentzen's LK proof system
Special cases of the interpolation theorem for classical predicate calculus
Forum: A multiple-conclusion specification logic
Some special cases of the interpolation theorem for intuitionistic predicate calculus
Permutability in proof terms for intuitionistic sequent calculus with cuts
Invertibility in Sequent Calculi
Coherence in Cartesian closed categories and the generality of proofs
Resolution is cut-free

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5813181)