Quantifier simplification by unification in SMT

DOI10.1007/978-3-030-86205-3_13OpenAlexW3197046268MaRDI QIDQ831945

Pascal Fontaine, Hans-Jörg Schurr

Publication date: 24 March 2022

Full work available at URL: https://orbi.uliege.be/handle/2268/265881

zbMATH Keywords

theorem provingSMTquantifier instantiation

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Uses Software

• VAMPIRE
• z3
• SIMPLIFY
• veriT
• CVC4
• AVATAR
• SMTCoq

Cites Work

• Unnamed Item
• Unnamed Item
• On deciding satisfiability by theorem proving with speculative inferences
• Reliable reconstruction of fine-grained proofs in a proof assistant
• SMTCoq: a plug-in for integrating SMT solvers into Coq
• Revisiting enumerative instantiation
• AVATAR: The Architecture for First-Order Theorem Provers
• Satisfiability Modulo Theories
• Congruence Closure with Free Variables
• Engineering DPLL(T) + Saturation
• Simplify: a theorem prover for program checking
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Efficient E-Matching for SMT Solvers
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• A Machine-Oriented Logic Based on the Resolution Principle

This page was built for publication: Quantifier simplification by unification in SMT