
Propositional
Resolution
and
Prime
Implicates
Generation
Title: 
Propositional Resolution and Prime Implicates Generation 
Author:

Nicolas Peltier

Submission date: 
20160311 
Abstract: 
We provide formal proofs in IsabelleHOL (using mostly structured Isar
proofs) of the soundness and completeness of the Resolution rule in
propositional logic. The completeness proofs take into account the
usual redundancy elimination rules (tautology elimination and
subsumption), and several refinements of the Resolution rule are
considered: ordered resolution (with selection functions), positive
and negative resolution, semantic resolution and unit resolution (the
latter refinement is complete only for clause sets that are Horn
renamable). We also define a concrete procedure for computing
saturated sets and establish its soundness and completeness. The
clause sets are not assumed to be finite, so that the results can be
applied to formulas obtained by grounding sets of firstorder clauses
(however, a total ordering among atoms is assumed to be given).
Next, we show that the unrestricted Resolution rule is deductive
complete, in the sense that it is able to generate all (prime)
implicates of any set of propositional clauses (i.e., all entailment
minimal, nonvalid, clausal consequences of the considered set). The
generation of prime implicates is an important problem, with many
applications in artificial intelligence and verification (for
abductive reasoning, knowledge compilation, diagnosis, debugging
etc.). We also show that implicates can be computed in an incremental
way, by fixing an ordering among all the atoms in the considered sets
and resolving upon these atoms one by one in the considered order
(with no backtracking). This feature is critical for the efficient
computation of prime implicates. Building on these results, we provide
a procedure for computing such implicates and establish its soundness
and completeness. 
BibTeX: 
@article{PropResPIAFP,
author = {Nicolas Peltier},
title = {Propositional Resolution and Prime Implicates Generation},
journal = {Archive of Formal Proofs},
month = mar,
year = 2016,
note = {\url{https://isaafp.org/entries/PropResPI.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
