Computing ground congruence classes

DOI10.1007/978-3-031-99984-0_31MaRDI QIDQ6869925zbMATH OpenFDO

Authors Hendrik Leidinger, Christoph Weidenbach

Publication date 21 January 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-99984-0_31

zbMATH Keywords

congruence closureequational reasoningfirst-order automated reasoning

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Cites work

• Automated reasoning building blocks
• Computer Aided Verification
• Congruence classes with logic variables
• Congruence closure with free variables
• Deciding Combinations of Theories
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• Fast congruence closure and extensions
• Fast Decision Procedures Based on Congruence Closure
• scientific article; zbMATH DE number 1765674 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Revisiting enumerative instantiation
• Rewriting
• SCL(EQ): SCL for first-order logic with equality
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• The MathSAT5 SMT solver
• The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Procee
• Variations on the Common Subexpression Problem

This page was built for publication: Computing ground congruence classes

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