Proof search in classical propositional logic with partial proof terms
From MaRDI portal
Cites work
- A coinductive approach to proof search through typed lambda-calculi
- A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
- Contextual modal type theory
- Control reduction theories: the benefit of structural substitution
- Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
- Decidability of several concepts of finiteness for simple types
- Dependent types and explicit substitutions: A meta-theoretical development
- Focusing and polarization in linear, intuitionistic, and classical logics
- scientific article; zbMATH DE number 1324438 (Why is no real title available?)
- scientific article; zbMATH DE number 1948185 (Why is no real title available?)
- scientific article; zbMATH DE number 2079018 (Why is no real title available?)
- scientific article; zbMATH DE number 786494 (Why is no real title available?)
- Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
- Logic Programming with Focusing Proofs in Linear Logic
- Mechanizing Mathematical Reasoning
- Normal natural deduction proofs (in classical logic)
- Partial proof terms in the study of idealized proof search
- Proof-term synthesis on dependent-type systems via explicit substitutions
- The duality of computation
- Towards a canonical classical natural deduction system
This page was built for publication: Proof search in classical propositional logic with partial proof terms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6876449)
