Extracting verified decision procedures: DPLL and Resolution

DOI10.2168/LMCS-11(1:6)2015zbMath1448.68454arXiv1502.02131MaRDI QIDQ5177337

Ulrich Berger, Fredrik Nordvall Forsberg, Monika Seisenberger, Andrew Lawrence

Publication date: 11 March 2015

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1502.02131

zbMATH Keywords

program extractionSATinteractive theorem provingDPLL

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Functional programming and lambda calculus (68N18) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Verifying the conversion into CNF in dafny ⋮ Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs

Uses Software

• Coq
• MiniSat
• Isabelle/HOL
• Metis_
• LLVM
• Chaff
• Sledgehammer
• versat
• Agda
• Minlog
• Idris

This page was built for publication: Extracting verified decision procedures: DPLL and Resolution