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

DOI10.1007/978-3-031-10769-6_14MaRDI QIDQ2104511zbMATH OpenOpenAlexFDO

Authors Hendrik Leidinger, Christoph Weidenbach

Publication date 7 December 2022

Copyright license Creative Commons Attribution 4.0 International

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)

Recommendations

• SCL(EQ): SCL for first-order logic with equality
• Equality reasoning in sequent-based calculi
• scientific article; zbMATH DE number 956469
• A theory of complete logic programs with equality
• scientific article; zbMATH DE number 826301
• Equational treatment of first-order logic
• On elementary equivalence for equality-free logic
• Computer Science Logic
• Infinitary equilibrium logic and strongly equivalent logic programs
• Two-variable first-order logic with equivalence closure

Cites work

• scientific article; zbMATH DE number 1189096 (Why is no real title available?)
• scientific article; zbMATH DE number 1303344 (Why is no real title available?)
• scientific article; zbMATH DE number 517065 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• scientific article; zbMATH DE number 3349331 (Why is no real title available?)
• A Computing Procedure for Quantification Theory
• A comprehensive framework for saturation theorem proving
• A machine program for theorem-proving
• Automated Deduction – CADE-20
• Automated reasoning building blocks
• Combining superposition, sorts and splitting
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• Fast Decision Procedures Based on Congruence Closure
• Hyper Tableaux with Equality
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Labelled unit superposition calculi for instantiation-based reasoning
• Lemma Learning in the Model Evolution Calculus
• Model evolution with equality -- revised and implemented
• NRCL -- a model building approach to the Bernays-Schönfinkel fragment
• On First-Order Model-Based Reasoning
• Ordered semantic hyper-linking
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Rewriting
• SCL clause learning from simple models
• Subsumption demodulation in first-order theorem proving
• Subterm contextual rewriting
• Superposition and Model Evolution Combined
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0

Cited in

(4)

• SCL(EQ): SCL for first-order logic with equality
• An Isabelle/HOL Formalization of the SCL(FOL) Calculus
• SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
• KBO Constraint Solving Revisited

Describes a project that uses

Uses Software

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

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

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