SCL clause learning from simple models

DOI10.1007/978-3-030-29436-6_14OpenAlexW2969435376MaRDI QIDQ2305416

Christoph Weidenbach, Alberto Fiori

Publication date: 10 March 2020

Full work available at URL: https://hal.inria.fr/hal-02405550/file/cade27.pdf

Mathematics Subject Classification ID

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

Related Items (9)

A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ SGGS decision procedures ⋮ A posthumous contribution by Larry Wos: excerpts from an unpublished column ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ SAT-Inspired Eliminations for Superposition

Cites Work

• Unnamed Item
• Semantically-guided goal-sensitive reasoning: model representation
• Deciding effectively propositional logic using DPLL and substitution sets
• Complete problems in the first-order predicate calculus
• Complexity results for classes of quantificational formulas
• The CADE-14 ATP system competition
• Non-cyclic Sorts for First-Order Satisfiability
• NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
• First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation
• Linear Integer Arithmetic Revisited
• Solving SAT and SAT Modulo Theories
• Proof Systems for Effectively Propositional Logic
• Superposition for Bounded Domains
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
• Lemma Learning in the Model Evolution Calculus
• Model Representation over Finite and Infinite Signatures

This page was built for publication: SCL clause learning from simple models