scientific article; zbMATH DE number 7378326
From MaRDI portal
Publication:5005105
DOI10.4230/LIPIcs.MFCS.2018.9MaRDI QIDQ5005105
Publication date: 4 August 2021
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
polarizationsequent calculusproof theoryautomated deductionlogic in computer sciencerefinements of resolutiondeduction modulo theory
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A logical characterization of forward and backward chaining in the inverse method
- Resolution is cut-free
- Focusing and polarization in linear, intuitionistic, and classical logics
- Handbook of proof theory
- Theorem proving modulo
- Regaining cut admissibility in deduction modulo using abstract completion
- Polarized Resolution Modulo
- The Proof Certifier Checkers
- Focused Labeled Proof Systems for Modal Logic
- Superdeduction at Work
- Truth Values Algebras and Proof Normalization
- Logic Programming with Focusing Proofs in Linear Logic
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Proof normalization modulo
- Foundational Proof Certificates in First-Order Logic
- Cut Admissibility by Saturation
- Experimenting with Deduction Modulo
- Automated Deduction – CADE-20
- Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
- Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
- Automatic Theorem Proving With Renamable and Semantic Resolution
- Term Rewriting and Applications
