Extracting a DPLL algorithm

DOI10.1016/J.ENTCS.2012.08.016MaRDI QIDQ3178287zbMATH OpenOpenAlexWikidataFDO

Authors Andrew Lawrence, Ulrich Berger, Monika Seisenberger

Publication date 8 July 2016

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2012.08.016

zbMATH Keywords

SATinteractive theorem provingprogram extractionDPLL

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Extracting verified decision procedures: DPLL and resolution
• Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus
• Extracting the resolution algorithm from a completeness proof for the propositional calculus
• Logic for Programming, Artificial Intelligence, and Reasoning
• scientific article; zbMATH DE number 5713654

Cites work

• scientific article; zbMATH DE number 1696436 (Why is no real title available?)
• scientific article; zbMATH DE number 5713654 (Why is no real title available?)
• scientific article; zbMATH DE number 1552509 (Why is no real title available?)
• scientific article; zbMATH DE number 3216998 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Advanced Functional Programming
• An arithmetic for non-size-increasing polynomial-time computation
• Combinatory logic. With two sections by William Craig.
• Decorating proofs
• GRASP: a search algorithm for propositional satisfiability
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Minlog -- a tool for program extraction supporting algebras and coalgebras
• Program extraction from normalization proofs
• Proofs and computations
• Sledgehammer: judgement day
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
• The relative efficiency of propositional proof systems

Cited in

(4)

• Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis
• Extracting the Resolution Algorithm from a Completeness Proof for the Propositional Calculus
• Extracting verified decision procedures: DPLL and resolution
• Extracting the resolution algorithm from a completeness proof for the propositional calculus

Describes a project that uses

Uses Software

• Minlog
• Agda
• Epigram
• Sledgehammer
• Chaff
• Metis
• Isabelle/HOL
• Isabelle
• Coq

This page was built for publication: Extracting a DPLL algorithm

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