Goal-oriented proof-search in natural deduction for intuitionistic propositional logic

DOI10.1007/S10817-017-9427-3zbMath1474.03067OpenAlexW2753667555MaRDI QIDQ1725847

Mauro Ferrari, Camillo Fiorentini

Publication date: 15 February 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-017-9427-3

zbMATH Keywords

natural deductionintuitionistic propositional logicproof-search procedures

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Subsystems of classical logic (including intuitionistic logic) (03B20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Correspondence analysis and automated proof-searching for first degree entailment

Uses Software

• ILTP
• fCube
• Imogen
• JTabWb
• IntHistGC
• intuit

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Yet another bijection between sequent calculus and natural deduction
• The \(\lambda \)-calculus and the unity of structural proof theory
• The ILTP problem library for intuitionistic logic
• Focusing and polarization in linear, intuitionistic, and classical logics
• Permutability of proofs in intuitionistic sequent calculi
• Normal natural deduction proofs (in classical logic)
• Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
• Uniform proofs as a foundation for logic programming
• ADC method of proof search for intuitionistic propositional natural deduction
• A Terminating Evaluation-Driven Variant of G3i
• Simplification Rules for Intuitionistic Propositional Tableaux
• An Evaluation-Driven Decision Procedure for G3i
• A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description
• Proof-Search in Natural Deduction Calculus for Classical Propositional Logic
• SAT Modulo Intuitionistic Implications
• JTabWb: a Java Framework for Implementing Terminating Sequent and Tableau Calculi
• Two loop detection mechanisms: A comparison
• Efficient loop-check for backward proof search in some non-classical propositional logics
• Focused Natural Deduction
• fCube: An Efficient Prover for Intuitionistic Propositional Logic
• An Intuitionistic Predicate Logic Theorem Prover
• Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
• Mechanizing Mathematical Reasoning
• Logical Approaches to Computational Barriers

This page was built for publication: Goal-oriented proof-search in natural deduction for intuitionistic propositional logic