非表示:
キーワード:
-
要旨:
We show that many properties studied in mathematical
analysis (monotonicity, boundedness, inverse, Lipschitz
properties, possibly combined with continuity or derivability)
are expressible by formulae in a class for which sound and
complete hierarchical proof methods for testing satisfiability of
sets of ground clauses exist.
The results are useful for automated reasoning in mathematical
analysis and for the verification of hybrid systems.
