Linking focusing and resolution with selection

DOI10.4230/LIPICS.MFCS.2018.9MaRDI QIDQ5005105zbMATH OpenFDO

Authors Guillaume Burel

Publication date 4 August 2021

Full work available at URL https://doi.org/10.4230/LIPICS.MFCS.2018.9

zbMATH Keywords

automated deductiondeduction modulo theorylogic in computer sciencepolarizationproof theoryrefinements of resolutionsequent calculus

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• Linking focusing and resolution with selection
• The focused calculus of structures
• A semantical analysis of focusing and contraction in intuitionistic logic
• Resolution is cut-free
• Structural focalization

Cites work

• A logical characterization of forward and backward chaining in the inverse method
• Automated Deduction – CADE-20
• Automatic Theorem Proving With Renamable and Semantic Resolution
• Cut Admissibility by Saturation
• Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
• Experimenting with deduction modulo
• Focused labeled proof systems for modal logic
• Focusing and polarization in linear, intuitionistic, and classical logics
• Foundational proof certificates in first-order logic
• Handbook of proof theory
• scientific article; zbMATH DE number 2086373 (Why is no real title available?)
• scientific article; zbMATH DE number 3254919 (Why is no real title available?)
• Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
• Logic Programming with Focusing Proofs in Linear Logic
• Polarized Resolution Modulo
• Proof normalization modulo
• Regaining cut admissibility in deduction modulo using abstract completion
• Resolution is cut-free
• Resolution theorem proving
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Superdeduction at Work
• Term Rewriting and Applications
• The Proof Certifier Checkers
• Theorem proving modulo
• Truth Values Algebras and Proof Normalization

Cited in

(2)

• scientific article; zbMATH DE number 1722713 (Why is no real title available?)
• Linking focusing and resolution with selection

Describes a project that uses

Uses Software

• Imogen
• Easychair

This page was built for publication: Linking focusing and resolution with selection

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