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

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

Authors: Hendrik Leidinger, Christoph Weidenbach 

Publication date: 7 December 2022

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

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

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

• Model evolution with equality -- revised and implemented
• Title not available (Why is that?)
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Ordered semantic hyper-linking
• Rewriting
• Combining superposition, sorts and splitting
• Title not available (Why is that?)
• 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
• Fast Decision Procedures Based on Congruence Closure
• On First-Order Model-Based Reasoning
• Automated Deduction – CADE-20
• Title not available (Why is that?)
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
• SCL clause learning from simple models
• Hyper Tableaux with Equality
• Title not available (Why is that?)
• Title not available (Why is that?)
• Subsumption demodulation in first-order theorem proving
• Automated reasoning building blocks
• NRCL -- a model building approach to the Bernays-Schönfinkel fragment
• A comprehensive framework for saturation theorem proving
• Subterm contextual rewriting
• Labelled unit superposition calculi for instantiation-based reasoning

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

Uses Software

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

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)