摘要:

In this work a new Automated Theorem Prover (ATP) via refutation for classical logic and which does not require the conversion to clausal form, named TAS-D++, is introduced. The main objective in the design of this ATP was to obtain a parallel and computationally efficient method naturally extensible to non-standard logics (concretely, to temporal logics, see [12]). TAS-D++works by using transformations of the syntactic trees of the formulas and, as tableaux and matrix style provers [6, 15, 16], it is Gentzen-based. Its power is mainly based in the efficient extraction of implicit information in the syntactic trees (in difference with the standard ATPs via refutation) to detect both:

ISSN:1166-3081    

DOI:10.1080/11663081.1995.10510841

出版商:Taylor & Francis Group    

年代:1995

数据来源: Taylor

摘要:

The main goal of this paper is to establish a nonmonotonic epistemic logic ϵβ with two modalities—provability and belief—capable of expressing and comparing a variety of known semantics for extended logic programs, and clarify their meaning. In particular we present here, for the first time, embeddings into epistemic logic of logic programs extended with a second kind of negation under the well-founded semantics, and contrast them to the recent embeddings into autoepistemic logics of such programs under stable models based semantics. Because of the newly established relationship between our epistemic logic ϵβ and extended program semantics, the former benefits from the procedures and implementations of the latter, and can be applied to at least the same class of AI problems that the latter can. Moreover, one issue of epistemic logic introduced here, belief revision, can profit from adapting techniques employed by the latter for contradiction removal. Furthermore, the language of the epistemic logic presented here being more general than that of extended programs, it offers a basic tool for further generalizations of the latter, for instance regarding disjunction and modal operators.

ISSN:1166-3081    

DOI:10.1080/11663081.1995.10510842

出版商:Taylor & Francis Group    

年代:1995

数据来源: Taylor

摘要:

In this paper, we argue that to apply rationality results of belief dynamics theory to various practical problems, it should be generalized in two respects: first of all, it should allow certain part of belief to be declared immutable; and secondly, the belief state need not be deductively closed. Such a generalization of belief dynamics, referred to as knowledge base dynamics, is presented, along with the concept of generalized contraction to contract a sentence from knowledge base. We show that knowledge base dynamics has interesting connections with abduction, thus enabling us to use abductive procedures to realize contractions. Finally, we demonstrate how knowledge base dynamics can provide an axiomatic characterization for deleting view atoms from databases.

ISSN:1166-3081    

DOI:10.1080/11663081.1995.10510843

出版商:Taylor & Francis Group    

年代:1995

数据来源: Taylor

摘要:

The major emphasis of this paper is on the definition of complete strategies in tableaux calculi for propositional modal logics. The strategies use a non exhaustive backtracking mechanism, a selective periodicity test and a uniform or a non uniform priority on the order of application of the tableaux rules. The propositional modal logics treated herein are those having a tableaux calculus with finite sets of formulas possibly occurring in the tableaux. Experimental results with the ATINF modal prover are presented.

ISSN:1166-3081    

DOI:10.1080/11663081.1995.10510844

出版商:Taylor & Francis Group    

年代:1995

数据来源: Taylor

摘要:

In this paper we describe a general way of formalizing reasoning behaviour. Such a behaviour may be described by all the patterns which are valid for the behaviour. A pattern can be seen as a sequence of information states which describe what has been derived at each time point. A transition from an information state at a point in time to the state at the (or a) next time point is induced by one or more inference steps. We choose to model the information states by partial models and the patterns either by linear time or branching time temporal models. Using temporal logic one can define theories and look at all models of that theory. For a number of examples of reasoning behaviour we have been able to define temporal theories such that its (minimal) models correspond to the valid patterns of the behaviour. These theories prescribe that the inference steps which are possible, are “executed” in the temporal model. The examples indicate that partial temporal logic is a powerful means of describing and formalizing complex reasoning patterns, as the dynamic aspects of reasoning systems are integrated into the static ones in a clear fashion.

ISSN:1166-3081    

DOI:10.1080/11663081.1995.10510845

出版商:Taylor & Francis Group    

年代:1995

数据来源: Taylor

摘要:

The aim of the present paper is to analyse compactness properties of nonmonotonic inference operations within the framework of model theory. For this purpose the concepts of a deductive frame and its semantical counterpart, a semantical frame are introduced. Compactness properties play a fundamental in the study of non-monotonic inference, and in the paper several new versions of compactness are studied.

ISSN:1166-3081    

DOI:10.1080/11663081.1995.10510846

出版商:Taylor & Francis Group    

年代:1995

数据来源: Taylor

摘要:

The instructions put together below fall into three categories. The editor of the review would be grateful to authors for respecting these indications. At times, the length of this summary may attain a dozen lines. It is to be written in size 9 italic Times. An abstract in French will be joined.

ISSN:1166-3081    

DOI:10.1080/11663081.1995.10510848

出版商:Taylor & Francis Group    

年代:1995

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.1995.10510849

出版商:Taylor & Francis Group    

年代:1995

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.1995.10510850

出版商:Taylor & Francis Group    

年代:1995

数据来源: Taylor

ISSN:1166-3081    

DOI:10.1080/11663081.1995.10510851

出版商:Taylor & Francis Group    

年代:1995

数据来源: Taylor