
David Botting; Waller Waller Guarini
Abstract: I will show that there is a type of analogical reasoning that instantiates a pattern of reasoning in confirmation theory that is considered at best paradoxical and at worst fatal to the entire syntactical approach to confirmation and explanation. However, I hope to elaborate conditions under which this is a sound (although not necessarily strong) method of reasoning. It does not, as its exponents claim, instantiate a pattern of reasoning distinct from deductive and inductive logic.

Valdez, Néstor Jorge; Falappa, Marcelo Alejandro
In logic programming, Horn clauses play a basic role, and in many logical constructs their consideration is important. In this paper we study the multiple revision of a belief base where the underlying logic is composed by Horn clauses. The main di culties as to restricting to the Horn fragment for revision operators by a single sentence are analyzed, and general results are presented about multiple revision operators on belief bases. We de ne prioritized multiple revision operators under a more restricted logic than classical propositional logic, i.e. Horn logic.
We propose a set of postulates and representation theorems for each...

Larshenrik Eriksson
Abstract. We describe how the calculus of partial inductive definitions is used to represent logics. This calculus includes the powerful principle of definitional reflection. We describe two conceptually different approaches to representing a logic, both making essential use of definitional reflection. In the deductive approach, the logic is defined by its inference rules. Only the succedent rules (in a sequent calculus setting – introduction rules in a natural deduction setting) need be given. The other rules are obtained implicitly using definitional reflection. In the semantic approach, the logic is defined using its valuation function. The latter approach often provides a...

Stephen Sharot
The rational choice theorists of religion have attempted to build upa body of transcultural, universalistic generalizations, be~nning with basic axioms ofhuman rationality. The problematics of the perspective's analytical focus on one type of rationality are ma & evident by a comparison u,ith Max Weber's types of action. The influence of the American reli~ous experience is evident in the perspective's formulations and explanations, and conceptual and theoretŸ problems arise when th perspective is applied to non.westem reli~on. The relationstª between otherwor/d/:y rewards and supernatural beings proposed by the theory has to bemodified with respect o eastem religions. Monopolista and pluralism take...

Yulia S. Korukhova; Postgraduate Student
In [Manna and Waldinger, 1992] the deductive tableau method was proposed. It is appropriate for the synthesis of functional programs. The specification of a program is taken as a mathematical existence theorem and we prove the existence of an object that satisfies the specified conditions. Specification is based on predicatelogic, because it is quite general and appropriate for deductive methods. If other

Ian K. Piumarta; Umcs Knowledgebased; Umcs An; Objectbased Design; Method Concurrent Programs
your order. Payment should be made by sterling cheque made payable to ‘The University of Manchester.’ The following reports are available free of charge, unless otherwise stated: UMCS9323 A Framework for Experimental Analysis of Parallel Computing

Bertil Rolf
Whatever the nature of reasoning skills, such skills are rare [4], [2]. Thus, it would be desirable to develop support for them and to cultivate and strengthen them through proper education in reasoning. The background for my discussion is the development of support for reasoning skills that our research team has been conducting for some time (www.athenasoft.org). Design of support or education for reasoning depends on concepts of reasoning skills. The essence of reasoning is to construct or evaluate relations of dependence. If D can be proved from A, B and C, there is a logical dependence between these items....

Keith Dromm; Crossfire (edward Dmytryk
While the literature on noir films is extensive, very little of it is devoted to the methods of its detectives and other characters that attempt to unravel the puzzles that typically lie at the heart of their plots.2 This might be because many believe that the noir investigators do not employ any methods.3 This is a view that has been held of their counterparts in the literary antecedents of film noir, the hardboiled detective stories and novels on which many noir films were based.4 The hardboiled detective was deliberately created to contrast with the classic detective; those detectives, as Raymond...

The paper describes a transition logic, TL, and a deductive formalism for it. It shows how various important aspects (such as ramification, qualification, specificity, simultaneity, indeterminism etc.) involved in planning can be modelled in TL in a rather natural way. (The deductive formalism for) TL extends the linear connection method proposed earlier by the author by embedding the latter into classical logic, so that classical and resourcesensitiv reasoning coexist within TL. The attraction of a logical and deductive approach to planning is emphasised and the state of automated deduction briefly described. 1

Pamela I. Ansburg; Leeann Shields
Participants underwent different kinds of training on the permission type of Wason's FourCard problem to determine whether transfer of general solution principles would occur to the arbitrary type of Wason's FourCard problem. There were four training conditions: (a) practice, (b) practice with feedback, (c) problem comparison only, and (d) problem comparison with feedback. Those participants who performed problem comparison on permission problems during practice solved more arbitrary problems during testing than did those participants who did not perform problem comparison. These findings suggest that through problem comparison participants learned how to apply general rules of logic from practice. Why does...

Teodor Przymusinski
We introduce 3valued stable models which are a natural generalization of standard (2valued) stable models. We show that every logic program P has at least one 3valued stable model and that the wellfounded model of any program P [VGRS90] coincides with the smallest 3valued stable model of P. We conclude that the wellfounded semantics of an arbitrary logic program coincides with the 3valued stable model semantics. The 3valued stable semantics is closely related to nonmonotonic formalisms in AI. Namely, every program P can be translated into a suitable autoepistemic (resp. default) theory P so that the 3valued stable semantics of...

Ulrich Endriss
In this paper we discuss how computers can be deployed to support teaching deductive reasoning at university level. These considerations led to the development of the interactive theorem proving assistant and learning environment WinKE. We start out by describing common difficulties in teaching logic and deductive reasoning and thereby justify the need for computer support in that field. We identify interaction (with a formal system) and visualisation (of abstract concepts) as two important components in a helpful pedagogical tool for teaching deductive reasoning. Thereafter the WinKE software, which deploys the logical calculus KE, is described. Important features include a comfortable...

Ulrich Endriss
WinKE is an interactive proof assistant based on the KE calculus, a refutation system which combines features from Smullyan’s analytic tableaux and Gentzen’s natural deduction. The software has been developed to support teaching logic and deductive reasoning at university level. In the sequel we brie‡y introduce the proof system KE and give an overview of the main features of the software tool. 1 The KE Calculus The KE calculus, developed by Mondadori and D’Agostino [2], is similar to the wellknown method of analytic tableaux in the sense that a theorem is shown by refuting its complement and the proof search...

Hashim Habiballa
The presentation deals with the refutational resolution theorem proving system for the Fuzzy Predicate Logic of FirstOrder (FPL) based on the general (nonclausal) resolution rule. It is based on the Fuzzy Predicate Logic with Evaluated Syntax. There is also presented an unification algorithm handling existentiality without the need of skolemization. Its idea follows from the general resolution with existentiality for the firstorder logic. When the prover is constructed it provides the deductive system, where existing resolution strategies and its implementations may be used with some limitations arising from specific properties of the FPL. Additionaly it presents recent advances in implementation...

Pavel Naumov
A new modal logic D is introduced. It describes properties of provability by interpreting modality as a deductive closure operator on sets of formulas. Logic D is proven to be decidable and complete with respect to this semantics. Key words: logic of provability, modal logic, deductive closure 1991 MSC: 03B45 1

Jeffrey D. Ullman
Deductive database systems  that is, database systems with a query language based on logical rules  must allow negated subgoals in rules to express an adequate range of queries. Adherence to classical deductive logic rarely offers the intuitively correct meaning of the rules. Thus,avariety of approaches to defining the "right" meaning of such rules have been developed. In this paper we survey the principal approaches, including stratified negation, wellfounded negation, stablemodel semantics, and modularly stratified semantics.

Anatoly Prihozhy; Liudmila Prihozhaya
This paper presents a new partial logic that generalizes the traditional proposition and first order predicate logics for incompletely specified domains. Three values are considered in the partial logic (false, true, and don’t care) instead of two values considered in the traditional logic. The operations, formulas, laws, and inference rules constitute a basis for knowledge representation and deductive reasoning when the world is not completely specified. The Robinson’s resolution principle is generalized for situation when a clause can take the don’t care value. Methods for the transition from partial deductive reasoning to inference in the first order predicate logic are...

Yannis Vassiliou; James Clifford; Matthias Jarke
As part of the operation of an Expert System, a deductive component accesses a database of facts to help simulate the behavior of a human expert in a particular problem domain. The nature of this access is examined, and four access strategies are identified. Features of each of these strategies are addressed within the framework of a Logicbased deductive component and the relational model of data.

Robert J. Simmons; Frank Pfenning; Robert J. Simmons; Frank Pfenning
Abstract. Bottomup logic programming can be used to declaratively specify many algorithms in a succinct and natural way, and McAllester and Ganzinger have shown that it is possible to define a cost semantics that enables reasoning about the running time of algorithms written as inference rules. Previous work with the programming language Lollimon demonstrates the expressive power of logic programming with linear logic in describing algorithms that have imperative elements or that must repeatedly make mutually exclusive choices. In this paper, we identify a bottomup logic programming language based on linear logic that is amenable to efficient execution and describe...

Velko Iltchev
Abstract: The paper proposes a seminaive method for processing recursive loops in the dependency graph for a given query. The process goes through two phases. During the expand phase answers are generated using translation to base conjunctions. Entries in recursive predicates with undistinguished arguments are also stored in the database for further processing. During the shrink phase the occurrences of recursive predicates in rulebodies are replaced with the answers already generated during the expand phase. Thus, the whole rulebody becomes a base conjunction, which generates new answers. The proposed method is suitable for queries with bound arguments. It reduces unnecessary...