scientific article; zbMATH DE number 5713654

MaRDI QIDQ3562927zbMATH OpenFDO

Authors Filip Marić, Predrag Janičić

Publication date 28 May 2010

Full work available at URL http://www.mii.lt/informatica/htm/INFO772.htm

zbMATH Keywords

DPLL procedureformal proofsIsabelleIsarSAT problem

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• scientific article; zbMATH DE number 107898
• Proof of Correctness of Decision Table Programs
• scientific article; zbMATH DE number 5917716
• scientific article; zbMATH DE number 877748
• Formal verification of a programming logic for a distributed programming language
• A completeness proof in full DDL
• Proving total correctness of recursive procedures
• scientific article; zbMATH DE number 1342248
• Proof of program correctness based on Kripke structure
• scientific article; zbMATH DE number 4076602

Cited in

(6)

• Extracting a DPLL algorithm
• Proof of Correctness of Decision Table Programs
• Using ÆtnaNova to formally prove that the Davis-Putnam satisfiability test is correct
• Extracting verified decision procedures: DPLL and resolution
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL
• Formalization and implementation of modern SAT solvers

Describes a project that uses

Uses Software

• Isabelle/Isar
• MiniSat
• Isar

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3562927)