Goal-Oriented Proof-Search in Natural Deduction for Intuitionistic Propositional Logic

2017 ◽  
Vol 62 (1) ◽  
pp. 127-167 ◽  
Author(s):  
Mauro Ferrari ◽  
Camillo Fiorentini
Keyword(s):  
Propositional Logic ◽  
Natural Deduction ◽  
Intuitionistic Propositional Logic ◽  
Proof Search

scholarly journals Efficient SAT-based Proof Search in Intuitionistic Propositional Logic

2021 ◽  
pp. 217-233
Author(s):  
Camillo Fiorentini
Keyword(s):  
Propositional Logic ◽  
Simple Structure ◽  
State Of The Art ◽  
Search Procedure ◽  
Intuitionistic Propositional Logic ◽  
Proof Search ◽  
Sat Solver

AbstractWe present an efficient proof search procedure for Intuitionistic Propositional Logic which involves the use of an incremental SAT-solver. Basically, it is obtained by adding a restart operation to the system by Claessen and Rosén, thus we call our implementation . We gain some remarkable advantages: derivations have a simple structure; countermodels are in general small; using a standard benchmarks suite, we outperform and other state-of-the-art provers.

scholarly journals Djinn, Monotonic

10.29007/33k5 ◽  
2018 ◽  
Author(s):  
Conor McBride
Keyword(s):  
Propositional Logic ◽  
Program Synthesis ◽  
Intuitionistic Propositional Logic ◽  
Proof Search ◽  
Compositional Approach ◽  
Termination Proof ◽  
Simple Program ◽  
Synthesis Tool ◽  
The Way

Dyckhoff's algorithm for contraction-free proof search in intuitionistic propositional logic (popularized by Augustsson as the type-directed program synthesis tool, Djinn) is a simple program with a rather tricky termination proof. In this talk, I describe my efforts to reduce this program to a steady structural descent. On the way, I shall present an attempt at a compositional approach to explaining termination, via a uniform presentation of memoization.

scholarly journals An Alternative Natural Deduction for the Intuitionistic Propositional Logic

2016 ◽  
Vol 45 (1) ◽  
Author(s):  
Mirjana Ilić
Keyword(s):  
Intuitionistic Logic ◽  
Propositional Logic ◽  
Natural Deduction ◽  
Sequent Calculus ◽  
Intuitionistic Propositional Logic ◽  
Deduction System ◽  
Natural Deduction System

A natural deduction system NI, for the full propositional intuitionistic logic, is proposed. The operational rules of NI are obtained by the translation from Gentzen’s calculus LJ and the normalization is proved, via translations from sequent calculus derivations to natural deduction derivations and back.

Sign in / Sign up

Export Citation Format

Share Document