Commit 88225a06 authored by Lawrence Paulson's avatar Lawrence Paulson
Browse files

new entry PropResPI

parent a4327c8e61df
This diff is collapsed.
This diff is collapsed.
chapter AFP
session "PropResPI" (AFP) = "HOL" +
options [timeout = 300, document = pdf]
# -*- shell-script -*-
# Get email when automated build fails. May be empty.
# values: "email1 email2 .. emailn"
# Participate in frequent (nightly) build (only for small submissions)
# values: "yes" "no"
% further packages required for unusual symbols (see also
% isabellesym.sty), use only when needed
%for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
%\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
%\<triangleq>, \<yen>, \<lozenge>
%for \<euro>
%for \<Sqinter>
%for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
%for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
% this should be the last package used
% urls in roman style, theory text in math-similar italics
% for uniform font size
\title{Propositional Resolution and Prime Implicates Generation}
\author{Nicolas Peltier\\Laboratory of Informatics of Grenoble/CNRS
\\University Grenoble Alps}
We provide formal proofs in Isabelle-HOL (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 (namely 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 first-order 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, non-valid, 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 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.
% sane default for proof documents
\parindent 0pt\parskip 0.5ex
% generated text of all theories
% optional bibliography
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
......@@ -189,6 +189,7 @@ Probabilistic_Noninterference
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment