SCL clause learning from simple models

DOI10.1007/978-3-030-29436-6_14MaRDI QIDQ2305416zbMATH OpenOpenAlexFDO

Authors Alberto Fiori, Christoph Weidenbach

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)

Recommendations

• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• NRCL -- a model building approach to the Bernays-Schönfinkel fragment
• An overview of resolution decision procedures
• scientific article; zbMATH DE number 1765665

Cites work

• scientific article; zbMATH DE number 1189096 (Why is no real title available?)
• Complete problems in the first-order predicate calculus
• Complexity results for classes of quantificational formulas
• Deciding effectively propositional logic using DPLL and substitution sets
• First-order logic theorem proving and model building via approximation and instantiation
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Lemma Learning in the Model Evolution Calculus
• Linear integer arithmetic revisited
• Model Representation over Finite and Infinite Signatures
• NRCL -- a model building approach to the Bernays-Schönfinkel fragment
• Non-cyclic sorts for first-order satisfiability
• Proof Systems for Effectively Propositional Logic
• Semantically-guided goal-sensitive reasoning: model representation
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• Superposition for bounded domains
• The CADE-14 ATP system competition

Cited in

(15)

• 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
• A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
• SCL(EQ): SCL for first-order logic with equality
• 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
• Exploring partial models with SCL
• First-order automatic literal model generation
• A modular formalization of superposition in Isabelle/HOL
• A stepwise refinement proof that SCL(FOL) simulates ground ordered resolution
• An Isabelle/HOL Formalization of the SCL(FOL) Calculus
• SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
• SAT-Inspired Eliminations for Superposition
• SGGS decision procedures

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2305416)