Combining decision procedures for the reals

DOI10.2168/LMCS-2(4:4)2006MaRDI QIDQ5310669zbMATH OpenFDO

Authors Jeremy Avigad, Harvey M. Friedman

Publication date 11 October 2007

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/LMCS-2(4:4)2006

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Deciding Combinations of Theories
• Decision algorithms for some fragments of analysis and related areas
• On the computational complexity and geometry of the first-order theory of the reals. III: Quantifier elimination
• Combined Decision Techniques for the Existential Theory of the Reals
• scientific article; zbMATH DE number 3898849

Cited in

(8)

• A general setting for flexibly combining and augmenting decision procedures
• A decision procedure for linear ``big O equations
• A heuristic prover for real inequalities
• Decidability of univariate real algebra with predicates for rational and integer powers
• Extending a Resolution Prover for Inequalities on Elementary Functions
• Combined Decision Techniques for the Existential Theory of the Reals
• Decision algorithms for some fragments of analysis and related areas
• scientific article; zbMATH DE number 512972 (Why is no real title available?)

This page was built for publication: Combining decision procedures for the reals

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