Simplification: A general constraint propagation technique for propositional and modal tableaux

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

Tableau and sequent calculi are the basis for most popular interactive theorem provers for formal verification. Yet, when it comes to automatic proof search, tableaux are often slower than Davis-Putnam, SAT procedures or other techniques. This is partly due to the absence of a bivalence principle (viz. the cut-rule) but there is another source of ineficiency: the lack of constraint propagation mechanisms. This paper proposes an innovation in this direction: the rule of simplification, which plays for tableaux the role of subsumption for resolution and of unit for the Davis-Putnam procedure. The simplicity and generality of simplification make possible its extension in a uniform way from propositional logic to a wide range of modal logics. This technique gives an unifying view of a number of tableaux-like calculi such as DPLL, KE, HARP, hyper-tableaux, BCP, KSAT. We show its practical impact with experimental results for random 3-SAT and the industrial IFIP benchmarks for hardware verification. © Springer-Verlag Berlin Heidelberg 1998.
Original languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods - International Conference, TABLEAUX 1998, Proceedings
PublisherSpringer Verlag
Pages217-231
DOIs
Publication statusPublished - 1998
Externally publishedYes
EventInternational Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 1998 - , Netherlands
Duration: 5 May 19988 May 1998

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 1998
Country/TerritoryNetherlands
Period5/05/988/05/98

Fingerprint

Dive into the research topics of 'Simplification: A general constraint propagation technique for propositional and modal tableaux'. Together they form a unique fingerprint.

Cite this