A Transformational Decision Procedure for Non-Clausal Propositional Formulas

Simple item page
dc.creatorSakharov, Alexander
dc.date2003-06-07
dc.date2003-06-16
dc.date.accessioned2026-07-07T03:19:47Z
dc.date.available2026-07-07T03:19:47Z
dc.descriptionA decision procedure for detecting valid propositional formulas is presented. It is based on the Davis-Putnam method and deals with propositional formulas that are initially converted to negational normal form. This procedure splits variables but, in contrast to other decision procedures based on the Davis-Putnam method, it does not branch. Instead, this procedure iteratively makes validity-preserving transformations of fragments of the formula. The transformations involve only a minimal formula part containing occurrences of the selected variable. Selection of the best variable for splitting is crucial in this decision procedure - it may shorten the decision process dramatically. A variable whose splitting leads to a minimal size of the transformed formula is selected. Also, the decision procedure performs plenty of optimizations based on calculation of delta-sets. Some optimizations lead to removing fragments of the formula. Others detect variables for which a single truth value assignment is sufficient. The latest information about this research can be found at http://www.sakharov.net/valid.html
dc.description12 pages
dc.identifierhttps://arxiv.org/abs/cs/0306035
dc.identifierhttp://arxiv.org/abs/cs/0306035
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/31602
dc.subjectLogic in Computer Science
dc.subjectComputational Complexity
dc.subjectF.4.1; F.2.2
dc.titleA Transformational Decision Procedure for Non-Clausal Propositional Formulas
dc.typetext

Files

Collections

arXiv