Conditional congruence closure over uninterpreted and interpreted symbols
type: Item
instance of: scholarly article
title: Conditional congruence closure over uninterpreted and interpreted symbols
zbMATH Open document ID: 1417.68077
author: Deepak Kapur
published in: Journal of Systems Science and Complexity
publication date: 2019-03-06T00:00:00Z
Mathematics Subject Classification ID: 68Q42
zbMATH DE Number: 7032440
zbMATH Keywords: completion
zbMATH Keywords: congruence closure
zbMATH Keywords: conditional congruence closure
zbMATH Keywords: intepreted symbols
zbMATH Keywords: rewriting
zbMATH Keywords: uninterpreted symbols
describes a project that uses: RRL
MaRDI profile type: Publication
full work available at URL: s11424-019-8377-8
OpenAlex ID: W2911667399
cites work: Variations on the Common Subexpression Problem
cites work: An algorithm for reasoning about equality
cites work: Fast Decision Procedures Based on Congruence Closure
cites work: Implementing contextual rewriting
cites work: Constraint solving for interpolation
cites work: Fast algorithms for testing unsatisfiability of ground Horn clauses with equations
cites work: Linear-time algorithms for testing the satisfiability of propositional horn formulae
cites work: Shostak's congruence closure as completion
cites work: Term Rewriting and All That
cites work: Efficiency of a Good But Not Linear Set Union Algorithm
cites work: An improved equivalence algorithm
cites work: Q5657644
cites work: Fast congruence closure and extensions
cites work: Complete Sets of Reductions for Some Equational Theories
cites work: Q3789100
cites work: Q4264723
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: Q5581665
cites work: Abstract congruence closure
cites work: Q4036569
cites work: Canonical Ground Horn Theories
cites work: On Shostak's decision procedure for combinations of theories
cites work: Q4518873
cites work: Any ground associative-commutative theory has a finite canonical system
cites work: Q3703293
cites work: On interpolation in automated theorem proving
cites work: Cover Algorithms and Their Combination
cites work: Q3338229
cites work: New decision algorithms for finitely presented commutative semigroups
Wikidata QID: Q128393049
DOI: 10.1007/S11424-019-8377-8
description: scientific article; zbMATH DE number 7032440