[isabelle] New in the AFP: Propositional Resolution

Iâm happy to announce yet another entry in the AFP. See the (shortened) abstract below. 

Itâs truly gratifying to see this collection of formal material grow and grow. We now have 268 entries and more than a million lines of formal proofs. And, with the help of the contributors and our own tools, we are able to keep all these entries working despite Isabelleâs rapid development.

Larry Paulson

Full name: Propositional Resolution and Prime Implicates Generation
Authors: Nicolas Peltier <http://membres-lig.imag.fr/peltier/>

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 (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.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.