SCL(EQ): SCL for first-order logic with equality

DOI10.1007/978-3-031-10769-6_14OpenAlexW4289104055MaRDI QIDQ2104511

Christoph Weidenbach, Hendrik Leidinger

Publication date: 7 December 2022

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

zbMATH Keywords

term rewritingfirst-order logic with equalitymodel-based reasoning

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

SCL(EQ): SCL for first-order logic with equality

Uses Software

• SPASS
• TPTP
• Darwin
• E-Darvin
• Chaff
• iProver-Eq
• iProver

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Model evolution with equality -- revised and implemented
• Ordered semantic hyper-linking
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Subsumption demodulation in first-order theorem proving
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• SCL clause learning from simple models
• On First-Order Model-Based Reasoning
• NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
• Automated Reasoning Building Blocks
• Subterm contextual rewriting
• Hyper Tableaux with Equality
• Fast Decision Procedures Based on Congruence Closure
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
• Labelled Unit Superposition Calculi for Instantiation-Based Reasoning
• Superposition and Model Evolution Combined
• Lemma Learning in the Model Evolution Calculus
• Automated Deduction – CADE-20
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A comprehensive framework for saturation theorem proving