Partial proof terms in the study of idealized proof search

DOI10.1007/978-3-031-66997-2_16MaRDI QIDQ6648177zbMATH OpenFDO

Authors José Espírito Santo, Ana Catarina Sousa

Publication date 4 December 2024

Full work available at URL https://doi.org/10.1007/978-3-031-66997-2_16

zbMATH Keywords

focusingintercalationpartial derivationpartial proof termproof searchproof state

Mathematics Subject Classification ID

Computer science support for mathematical research and practice (68Vxx)

Cites work

• A coinductive approach to proof search through typed lambda-calculi
• A Linear Spine Calculus
• A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems
• A short note on type-inhabitation: formula-trees vs. game semantics
• Automata theoretic account of proof search
• Contextual modal type theory
• 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
• Game semantics and uniqueness of type inhabitance in the simply-typed -calculus
• scientific article; zbMATH DE number 48365 (Why is no real title available?)
• scientific article; zbMATH DE number 1948185 (Why is no real title available?)
• scientific article; zbMATH DE number 1980937 (Why is no real title available?)
• scientific article; zbMATH DE number 2079018 (Why is no real title available?)
• scientific article; zbMATH DE number 1390270 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search
• Lectures on the Curry-Howard isomorphism
• Logical Approaches to Computational Barriers
• Mechanizing Mathematical Reasoning
• Normal natural deduction proofs (in classical logic)
• Normal proofs and their grammar
• Proof-term synthesis on dependent-type systems via explicit substitutions
• The \(\lambda \)-calculus and the unity of structural proof theory
• The polarized \(\lambda\)-calculus
• Towards a canonical classical natural deduction system
• Uniform proofs as a foundation for logic programming

Cited in

(1)

• Proof search in classical propositional logic with partial proof terms

This page was built for publication: Partial proof terms in the study of idealized proof search

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