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 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 On density of truth of the intuitionistic logic in one variable

2008 ◽  
Vol DMTCS Proceedings vol. AI,... (Proceedings) ◽  
Author(s):  
Zofia Kostrzycka
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Propositional Logic ◽  
Propositional Variable ◽  
Intuitionistic Propositional Logic ◽  
International Audience

International audience In this paper we focus on the intuitionistic propositional logic with one propositional variable. More precisely we consider the standard fragment $\{ \to ,\vee ,\bot \}$ of this logic and compute the proportion of tautologies among all formulas. It turns out that this proportion is different from the analog one in the classical logic case.

Sign in / Sign up

Export Citation Format

Share Document