1,721,373 research outputs found
Using Abstrips Abstraction - Where do we stand?
No full textMany experimental and theoretical results have been provided which analyze the effects of Abstrips abstractions in search problems. Some of these results are positive, i.e. show gains in efficiency; some are negative and seem to contradict, at least partially, the positive results. The aim of this note is to provide an analysis of how Abstrips abstractions work, and use it to provide an explanation of the main results which can be found in the literatur
Local Models Semantics, or Contextual Reasoning = Locality + Compatibility
No full textIn this paper we present a new semantics, called Local Models Semantics, and use it to provide a foundation to reasoning with contexts. This semantics captures and makes precise the two main intuitions underlying contextual reasoning: (i) reasoning is mainly local and uses only part of what is potentially avilable (e.g. what is known, the available interference procedures), this part is what we call context (of reasoning), however (ii) the context may change and there is compatibility among the reasoning performed in different contexts. We validate or semantics by formalizing two important forms of contextual reasoning: reasoning with viewpoints and reasoning about belie
Reasoning about Theory Formulation and Reformulation. A New Solution to the Qualification Problem
No full textOne of the main problems in formalizing common sense reasoning is the qualification problem, i.e. the fact that the truth of many general sentences depends on a virtually infinite number of qualifications. Traditionally, this has been seen as the problem of computing the set of qualifications which are entailed by a given knowledge base, and then of expressing the conjecture that these are all the qualifications which must be considered. In this paper, we argue that a preliminary step should be that of restricting the focus on an adequate subset of a (potentially) very large knowledge base; that the adequacy of such a subset can only be conjectured depending on the formulation of the problem to be solved; and that this conjecture can be defeated whenever new information is added. We show how this can be achieved using a mechanism of ‘theory formulation’ and ‘reformulation’ in the framework of MultiContext Systems. As an anecdotal example, we present a solution to McCarthy’s Glasgow-London-Moscow proble
A metatheory of a mechanized object theory
No full textAbstractIn this paper we propose a metatheory, MT, which represents the computation which implements its object theory, OT, and, in particular, the computation which implements deduction in OT. To emphasize this fact we say that MT is a metatheory of a mechanized object theory. MT has some “unusual” properties, e.g. it explicitly represents failure in the application of inference rules, and the fact that large amounts of the code implementing OT are partial, i.e. they work only for a limited class of inputs. These properties allow us to use MT to express and prove tactics, i.e. expressions which specify how to compose possibly failing applications of inference rules, to interpret them procedurally to assert theorems in OT, to compile them into the system implementation code, and, finally, to generate MT automatically from the system code. The definition of MT is part of a larger project which aims at the implementation of self-reflective systems, i.e. systems which are able to introspect their own code, to reason about it and, possibly, to extend or modify it
A Local Models Semantics for Propositional Attitudes
No full textOur starting point is a formulation of modal logics, described in previous papers, defined in terms of a hierarchy of distinct (that is, not amalgamated) metatheories. These logics, called Hierarchical Multilanguage Belief (HMB) systems formalize the current practice in the implementation of propositional attitudes, and in particular belief, inside complex reasoning systems. Our goal is to define e new semantics for HMB systems, called local models semantics, which captures their underlying intuitions. In local models semantics each (meta)theory defines a set of first order models, called ‘local models’; belief is a unary predicate; and the extension of the belief predicate is computed by enforcing constraints among sets of local model
From Tableau-based to SAT-based procedures - preliminary report
No full textTableau systems are very popular in AI for their simplicity and versatility. In recent papers we showed that tableau-based procedures are intrinsically inefficient, and proposed an alternative approach of building decision procedures on top of SAT decision procedure. We called this approach ‘SAT based’. In extensive empirical tests on the case study of modal K, a SAT-based procedure drastically outperformed a state-of-the-art tableau-based system. In this paper we provide the theoretical foundations for developing SAT-based decision procedures for many different modal logic
ML systems: A Proof Theory for Contexts
Full text linkIn the last decade the concept of context has been extensively exploited in many research areas, e.g., distributed artificial intelligence, multi agent systems, distributed databases, information integration, cognitive science, and epistemology. Three alternative approaches to the formalization of the notion of context have been proposed: Giunchiglia and Serafini's Multi Language Systems (ML systems), McCarthy's modal logics of contexts, and Gabbay's Labelled Deductive Systems. Previous papers have argued in favor of ML systems with respect to the other approaches. Our aim in this paper is to support these arguments from a theoretical perspective. We provide a very general definition of ML systems, which covers all the ML systems used in the literature, and we develop a proof theory for an important subclass of them: the MR systems. We prove various important results; among other things, we prove a normal form theorem, the sub-formula property, and the decidability of an important instance of the class of the MR systems. The paper concludes with a detailed comparison among the alternative approaches
A Metatheory of a Mechnized Object Theory
No full textThe goal of this paper is to propose a metatheory, MT which describes the computation which carries out deduction in the object theory. MT is proved to have some `standard` properties, eg. it is consistent and is is such that theoremhood of the name of
- …
