Congruence closure with free variables

DOI10.1007/978-3-662-54580-5_13MaRDI QIDQ3303931zbMATH OpenOpenAlexFDO

Authors Haniel Barbosa, Pascal Fontaine, Andrew Reynolds

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)

Recommendations

• \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Fast congruence closure and extensions
• Solving quantified verification conditions using satisfiability modulo theories
• SMELS: Satisfiability Modulo Equality with Lazy Superposition

Cites work

• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• E-matching with free variables
• Efficient algorithms for bounded rigid E-unification
• Efficient E-Matching for SMT Solvers
• Engineering DPLL(T) + Saturation
• Equality reasoning in sequent-based calculi
• Fast congruence closure and extensions
• Fast Decision Procedures Based on Congruence Closure
• scientific article; zbMATH DE number 46359 (Why is no real title available?)
• scientific article; zbMATH DE number 517077 (Why is no real title available?)
• scientific article; zbMATH DE number 1552529 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Quantifier instantiation techniques for finite model finding in SMT
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Simplify: a theorem prover for program checking
• Term Rewriting and All That
• Theorem proving with bounded rigid E-unification

Cited in

(14)

• Computing congruent closures on terms
• Reliable reconstruction of fine-grained proofs in a proof assistant
• Incremental search for conflict and unit instances of quantified formulas with E-matching
• Extending SMT solvers to higher-order logic
• Fault-tolerant aggregate signatures
• \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
• E-matching with free variables
• SAT-Inspired Eliminations for Superposition
• Scalable fine-grained proofs for formula processing
• Clausal congruence closure
• Computing ground congruence classes
• Substitutions for Lambda-Free Higher-Order Terms
• Quantifier simplification by unification in SMT
• Theory exploration powered by deductive synthesis

Describes a project that uses

Uses Software

• SIMPLIFY
• veriT
• z3
• CVC4
• GRASShopper

This page was built for publication: Congruence closure with free variables

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