1,721,017 research outputs found
The Bernays-Schoenfinkel-Ramsey Class in Set Theory: Decidability
No full textAs proved recently. the satisfaction problem for all prenex formulae in the set-theoretic Bernays-Shonfinkel-Ramsey class is semi-decidable over von Neumann's cumulative hierarchy. Here that semi-decidability result is strengthened into a decidability result for the same collection of formulae
The Automation of Syllogistic II. Optimization and Complexity Issues
Full text linkIn the first paper of this series it was shown that any unquantified formula p in the collection MLSSF (multilevel syllogistic extended with the singleton operator and the predicate Finite) can be decomposed as a disjunction of set-theoretic formulae called syllogistic schemes. The syllogistic schemes are satisfiable and no two of them have a model in common, therefore the previous result already implied the decidability of the class MLSSF by simply checking if the set of syllogistic schemes associated with the given formula is empty. In the first section of this paper a new and improved searching algorithm for syllogistic schemes is introduced, based on a proof of existence of a 'minimum effort' scheme for any given satisfiable formula in MLSF. The algorithm addressed above can be piloted quite effectively even though it involves backtracking. In the second part of the paper, complexity issues are studied by showing that the class of (∀)o1-simple prenex formulae (an extension of MLS) has a decision problem which is NP-complete. The decision algorithm that proves the membership of this decision problem to NP can be seen as a different decision algorithm for ML
A Sound and Complete Validity Test for Formulas in Extensional Multi-level Syllogistic
No full textIn this paper we introduce both the syntax and the semantics of a formal language which has been designed to express multi-level syllogistic
A graphical approach to relational reasoning
Full text linkRelational reasoning is concerned with relations over an unspecified domain of discourse. Two limitations to which it is customarily subject are: only dyadic relations are taken into account; all formulas are equations, having the same expressive power as first-order sentences in three variables. The relational formalism inherits from the Peirce-Schröder tradition, through contributions of Tarski and many others. Algebraic manipulation of relational expressions (equations in particular) is much less natural than developing inferences in first-order logic; it may in fact appear to be overly machine-oriented for direct hand-based exploitation. The situation radically changes when one resorts to a convenient representation of relations based on labeled graphs. The paper provides details of this representation, which abstracts w.r.t. inessential features of expressions. Formal techniques illustrating three uses of the graph representation of relations are discussed: one technique deals with translating first-order specifications into the calculus of relations; another one, with inferring equalities within this calculus with the aid of convenient diagram-rewriting rules; a third one with checking, in the specialized framework of set theory, the definability of particular set operations. Examples of use of these techniques are produced; moreover, a promising approach to mechanization of graphical relational reasoning is outlined
Layered map reasoning An experimental approach put to trial on sets1 1This research was partially funded by the Italian IASI-CNR (coordinated project log(SETA)) and by MURST (PGR-2000—Automazione del ragionamento in teorie insiemistiche).
Full text linkAbstractNew successes in dealing with set-theories by means of state-of-the-art theorem-provers may ensue from terse and concise axiomatic systems, such as can be moulded in the framework of the (fully equational) Tarski-Givant formalism of dyadic relations, here named ‘maps’. This paper sets the ground for systematic experimentation based on such axiomatic systems. On top of a kernel axiomatization of map algebra, we develop a layered formalization of basic set-theoretic concepts. A number of concrete experiments have been carried out in this framework, as the paper reports, with the assistance of a first-order theorem-prover. The aim is to assess the potential usefulness of the proposed layered architecture and, to the extent it reveals promising, to best tune it
- …
