Quantifier simplification by unification in SMT

DOI10.1007/978-3-030-86205-3_13MaRDI QIDQ831945zbMATH OpenOpenAlexFDO

Authors 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

SMTtheorem provingquantifier instantiation

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Cites work

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

Cited in

(3)

• scientific article; zbMATH DE number 1253959 (Why is no real title available?)
• On simplification of formulas with unconstrained variables and quantifiers
• SAT Encoding of Unification in $\mathcal{EL}$

Describes a project that uses

Uses Software

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

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

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