Extracting a DPLL Algorithm

DOI10.1016/j.entcs.2012.08.016zbMath1342.68293OpenAlexW1986342613WikidataQ113318074 ScholiaQ113318074MaRDI QIDQ3178287

Andrew Lawrence, Monika Seisenberger, Ulrich Berger

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

program extractionSATinteractive theorem provingDPLL

Mathematics Subject Classification ID

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

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Combinatory logic. With two sections by William Craig.
• Program extraction from normalization proofs
• Isabelle. A generic theorem prover
• The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
• Isabelle/HOL. A proof assistant for higher-order logic
• An arithmetic for non-size-increasing polynomial-time computation
• Minlog - A Tool for Program Extraction Supporting Algebras and Coalgebras
• Proofs and Computations
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Source-Level Proof Reconstruction for Interactive Theorem Proving
• The relative efficiency of propositional proof systems
• GRASP: a search algorithm for propositional satisfiability
• Advanced Functional Programming
• Sledgehammer: Judgement Day