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

DOI10.1007/s10817-023-09673-3MaRDI QIDQ6111523

Christoph Weidenbach, Hendrik Leidinger

Publication date: 4 August 2023

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

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)

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
• SCL(EQ): SCL for first-order logic with equality
• 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
• Solving SAT and SAT Modulo Theories
• Subterm contextual rewriting
• Hyper Tableaux with Equality
• Fast Decision Procedures Based on Congruence Closure
• An algorithm for finding canonical sets of ground rewrite rules in polynomial time
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Inst-Gen – A Modular Approach to Instantiation-Based Automated 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
• iProver-Eq: An Instantiation-Based Theorem Prover with Equality
• A comprehensive framework for saturation theorem proving

This page was built for publication: SCL(EQ): SCL for first-order logic with equality