Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
type: Item
instance of: scholarly article
title: Goal-oriented proof-search in natural deduction for intuitionistic propositional logic
zbMATH Open document ID: 1474.03067
author: Mauro Ferrari
author: Camillo Fiorentini
published in: Journal of Automated Reasoning
publication date: 2019-02-15T00:00:00Z
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B20
Mathematics Subject Classification ID: 03F07
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7024054
zbMATH Keywords: natural deduction
zbMATH Keywords: intuitionistic propositional logic
zbMATH Keywords: proof-search procedures
describes a project that uses: JTabWb
describes a project that uses: IntHistGC
describes a project that uses: Imogen
describes a project that uses: ILTP
describes a project that uses: intuit
describes a project that uses: fCube
MaRDI profile type: Publication
full work available at URL: s10817-017-9427-3
OpenAlex ID: W2753667555
cites work: Focused Natural Deduction
cites work: Q3128959
cites work: SAT Modulo Intuitionistic Implications
cites work: Logical Approaches to Computational Barriers
cites work: Permutability of proofs in intuitionistic sequent calculi
cites work: Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
cites work: Yet another bijection between sequent calculus and natural deduction
cites work: Proof-Search in Natural Deduction Calculus for Classical Propositional Logic
cites work: fCube: An Efficient Prover for Intuitionistic Propositional Logic
cites work: Simplification Rules for Intuitionistic Propositional Tableaux
cites work: A Terminating Evaluation-Driven Variant of G3i
cites work: An Evaluation-Driven Decision Procedure for G3i
cites work: JTabWb: a Java Framework for Implementing Terminating Sequent and Tableau Calculi
cites work: A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description
cites work: Q4474830
cites work: Efficient loop-check for backward proof search in some non-classical propositional logics
cites work: Two loop detection mechanisms: A comparison
cites work: Focusing and polarization in linear, intuitionistic, and classical logics
cites work: Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic
cites work: Uniform proofs as a foundation for logic programming
cites work: ADC method of proof search for intuitionistic propositional natural deduction
cites work: Q5559220
cites work: The ILTP problem library for intuitionistic logic
cites work: An Intuitionistic Predicate Logic Theorem Prover
cites work: The \(\lambda \)-calculus and the unity of structural proof theory
cites work: Normal natural deduction proofs (in classical logic)
cites work: Mechanizing Mathematical Reasoning
cites work: Q4499084
DOI: 10.1007/S10817-017-9427-3
description: scientific article; zbMATH DE number 7024054