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 Bringing Order to Chaos – A Compact Representation of Partial Order in SAT-Based HTN Planning

2019 ◽  
Vol 33 ◽  
pp. 7520-7529 ◽  
Author(s):  
Gregor Behnke ◽  
Daniel Höller ◽  
Susanne Biundo
Keyword(s):  
Partial Order ◽  
Propositional Logic ◽  
State Of The Art ◽  
Partial Ordering ◽  
Compact Representation ◽  
Planning Techniques ◽  
Model Complex ◽  
Htn Planning ◽  
Sat Solver ◽  
Planning Problems

HTN planning provides an expressive formalism to model complex application domains. It has been widely used in realworld applications. However, the development of domainindependent planning techniques for such models is still lacking behind. The need to be informed about both statetransitions and the task hierarchy makes the realisation of search-based approaches difficult, especially with unrestricted partial ordering of tasks in HTN domains. Recently, a translation of HTN planning problems into propositional logic has shown promising empirical results. Such planners benefit from a unified representation of state and hierarchy, but until now require very large formulae to represent partial order. In this paper, we introduce a novel encoding of HTN Planning as SAT. In contrast to related work, most of the reasoning on ordering relations is not left to the SAT solver, but done beforehand. This results in much smaller formulae and, as shown in our evaluation, in a planner that outperforms previous SAT-based approaches as well as the state-of-the-art in search-based HTN planning.

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.

Sign in / Sign up

Export Citation Format

Share Document