Combining decision procedures for the reals

DOI10.2168/LMCS-2(4:4)2006zbMath1127.03006MaRDI QIDQ5310669

Harvey M. Friedman, Jeremy Avigad

Publication date: 11 October 2007

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

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)

Related Items (3)

A heuristic prover for real inequalities ⋮ A decision procedure for linear ``big O equations ⋮ Extending a Resolution Prover for Inequalities on Elementary Functions

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