Email Gateway (Aug 22 2022 at 12:57): Email Gateway (Aug 22 2022 at 12:57):From: Lawrence Paulson <lp15@cam.ac.uk>
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.
Last updated: Nov 21 2024 at 12:39 UTC