Loading...
Please wait, while we are loading the content...
Similar Documents
A tableau calculus for integrating first-order and elementary set theory reasoning (2000).
| Content Provider | CiteSeerX |
|---|---|
| Author | Cantone, Domenico Zarba, Calogero G. Doria, Viale A. |
| Abstract | . In this paper we describe an approach to integrate rstorder reasoning with stratied set theory reasoning, resulting into a technique which allows to lift decision procedures for ground theories to 98-sentences and combine them also with elementary set constructs, such as union, intersection, nite enumerations, membership, inclusion, equality, and monotonicity predicates over function maps. A tableau calculus, both sound and complete, is provided. The calculus is proven complete also in presence of suitable restrictions which enforce termination, thus yielding decision procedures in certain cases. 1 Introduction Most of the work in computable set theory has concentrated on the decision problem for fragments of Zermelo-Fraenkel set theory, in presence of foundation or anti-foundation axiom (cf. [4] and [5]). Some exceptions are [10], [6], [3], and [2], where decision procedures have been provided for fragments of stratied set theory, and precisely for (1) a quantierfree... |
| File Format | |
| Publisher Date | 2000-01-01 |
| Access Restriction | Open |
| Subject Keyword | Tableau Calculus Integrating First-order Decision Procedure Elementary Set Theory Reasoning Decision Problem Elementary Set Construct Stratied Set Theory Monotonicity Predicate Function Map Anti-foundation Axiom Certain Case Zermelo-fraenkel Set Theory Stratied Set Theory Reasoning Nite Enumeration Suitable Restriction Computable Set Theory Ground Theory |
| Content Type | Text |
| Resource Type | Article |
