Automated Reasoning Building Blocks

DOI10.1007/978-3-319-23506-6_12zbMath1444.68289OpenAlexW1881903642MaRDI QIDQ3449631

Christoph Weidenbach

Publication date: 4 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-23506-6_12

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (6)

A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ A complete and terminating approach to linear integer solving ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ SCL(EQ): SCL for first-order logic with equality

Uses Software

• Darwin
• Chaff

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Deciding effectively propositional logic using DPLL and substitution sets
• A Resolution Calculus for First-order Schemata
• NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
• First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation
• Solving SAT and SAT Modulo Theories
• Lemma Learning in the Model Evolution Calculus
• A Machine-Oriented Logic Based on the Resolution Principle
• A machine program for theorem-proving

This page was built for publication: Automated Reasoning Building Blocks