Generating and Exploiting Automated Reasoning Proof Certificates
Haniel Barbosa, Clark Barrett, Byron Cook, Bruno Dutertre, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar
Abstract
Moving toward a full suite of proof-producing automated reasoning tools with SMT solvers that can produce full, independently checkable proofs for real-world problems.
Topics & Concepts
Mathematical proofComputer scienceSuiteAutomated reasoningProof of conceptAutomated proof checkingProof complexityProgramming languageProof assistantAutomated theorem provingProof theoryReasoning systemSoftware engineeringTheoretical computer scienceMathematicsOperating systemArchaeologyGeometryHistoryLogic, programming, and type systemsFormal Methods in VerificationLogic, Reasoning, and Knowledge