Congruence Closure with Free Variables

DOI10.1007/978-3-662-54580-5_13zbMath1452.68113OpenAlexW2598379852MaRDI QIDQ3303931

Pascal Fontaine, Andrew Reynolds, Haniel Barbosa

Publication date: 5 August 2020

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01442691/file/main.pdf

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

Quantifier simplification by unification in SMT ⋮ Theory exploration powered by deductive synthesis ⋮ Incremental search for conflict and unit instances of quantified formulas with E-matching ⋮ Fault-Tolerant Aggregate Signatures ⋮ Scalable fine-grained proofs for formula processing ⋮ Reliable reconstruction of fine-grained proofs in a proof assistant ⋮ Extending SMT solvers to higher-order logic ⋮ SAT-Inspired Eliminations for Superposition

Uses Software

• z3
• SIMPLIFY
• veriT
• CVC4
• GRASShopper

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Fast congruence closure and extensions
• E-Matching with Free Variables
• Theorem Proving with Bounded Rigid E-Unification
• Efficient Algorithms for Bounded Rigid E-unification
• Engineering DPLL(T) + Saturation
• Simplify: a theorem prover for program checking
• Efficient E-Matching for SMT Solvers
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Fast Decision Procedures Based on Congruence Closure
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Term Rewriting and All That
• Quantifier Instantiation Techniques for Finite Model Finding in SMT