On simplification of formulas with unconstrained variables and quantifiers

DOI10.1007/978-3-319-66263-3_23MaRDI QIDQ1680265zbMATH OpenOpenAlexFDO

Authors Martin Jonáš, Jan Strejček

Publication date 15 November 2017

Full work available at URL https://doi.org/10.1007/978-3-319-66263-3_23

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Simplification of quantifier-free formulae over ordered fields
• Simplification rules for constrained formula tableaux
• Formula Simplification for Real Quantifier Elimination Using Geometric Invariance
• On simplifying truth-functional formulas
• On simplicity of formulas
• Quantifier simplification by unification in SMT
• scientific article; zbMATH DE number 1263329
• Simplifications of Uniform Expressions Specified by Systems
• scientific article; zbMATH DE number 1670829
• SAT-Based Formula Simplification

Cited in

(4)

• Simplification of quantifier-free formulae over ordered fields
• Formula Simplification for Real Quantifier Elimination Using Geometric Invariance
• Simplifications of Uniform Expressions Specified by Systems
• Truncating abstraction of bit-vector operations for BDD-based SMT solvers

This page was built for publication: On simplification of formulas with unconstrained variables and quantifiers

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