Pages that link to "Item:Q876046"
From MaRDI portal
The following pages link to Fast congruence closure and extensions (Q876046):
Displaying 27 items.
- Theory exploration powered by deductive synthesis (Q832255) (← links)
- Fast algorithms for testing unsatisfiability of ground Horn clauses with equations (Q1100933) (← links)
- Computing congruent closures on terms (Q1280915) (← links)
- Abstract congruence closure (Q1425161) (← links)
- NP-completeness of small conflict set generation for congruence closure (Q1688538) (← links)
- Conditional congruence closure over uninterpreted and interpreted symbols (Q1730315) (← links)
- Model completeness, uniform interpolants and superposition calculus. (With applications to verification of data-aware processes) (Q2051565) (← links)
- Deciding the word problem for ground and strongly shallow identities w.r.t. extensional symbols (Q2090128) (← links)
- Deciding the word problem for ground identities with commutative and extensional symbols (Q2096444) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- Extending SMT solvers to higher-order logic (Q2305406) (← links)
- Congruence classes with logic variables (Q2708308) (← links)
- Fault-Tolerant Aggregate Signatures (Q2798782) (← links)
- Justifying equality (Q2848059) (← links)
- Model-based theory combination (Q2864402) (← links)
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories (Q2864404) (← links)
- Satisfiability Modulo Theories (Q3176369) (← links)
- New (Q3178271) (← links)
- Congruence Closure with Free Variables (Q3303931) (← links)
- Modal Tableau Systems with Blocking and Congruence Closure (Q3455760) (← links)
- (Q4553285) (← links)
- Efficient Interpolant Generation in Satisfiability Modulo Theories (Q5458340) (← links)
- An Automata View to Goal-Directed Methods (Q5738990) (← links)
- Fast LCF-Style Proof Reconstruction for Z3 (Q5747649) (← links)
- Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties (Q6135743) (← links)
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover (Q6156634) (← links)
- Invariant neural architecture for learning term synthesis in instantiation proving (Q6650564) (← links)
