NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment

DOI10.1007/978-3-319-24246-0_5zbMath1471.03013arXiv1502.05501OpenAlexW1927589922MaRDI QIDQ2964454

Christoph Weidenbach, Gábor Alagi

Publication date: 27 February 2017

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items (11)

Automated Reasoning Building Blocks ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ SCL clause learning from simple models ⋮ A complete and terminating approach to linear integer solving ⋮ SGGS decision procedures ⋮ An efficient subsumption test pipeline for BS(LRA) clauses ⋮ SCL(EQ): SCL for first-order logic with equality

Uses Software

• MiniSat
• Darwin
• iProver
• YAGO

Cites Work

• Automated reasoning. 4th international joint conference, IJCAR 2008, Sydney, Australia, August 12--15, 2008 Proceedings
• Deciding effectively propositional logic using DPLL and substitution sets
• Labelled splitting
• Explicit representation of terms defined by counter examples
• Complexity results for classes of quantificational formulas
• Non-cyclic Sorts for First-Order Satisfiability
• NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• 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
• Logic for Programming, Artificial Intelligence, and Reasoning
• On the Saturation of YAGO
• Ordering by Divisibility in Abstract Algebras
• Automated Deduction – CADE-19
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment