Conditional and Preferential Logics: Proof Methods and Theorem Proving

This document was uploaded by one of our users. The uploader already confirmed that they had the permission to publish it. If you are author/publisher or own the copyright of this documents, please report to us by using this DMCA report form.

Simply click on the Download Book button.

Yes, Book downloads on Ebookily are 100% Free.

Sometimes the book is free on Amazon As well, so go ahead and hit "Search on Amazon"

This volume contains a revised and updated version of the authors Ph.D. dissertation and is focused on proof methods and theorem proving for conditional and preferential logics. Conditional logics are extensions of classical logic by means of a conditional operator, usually denoted as =>. Conditional logics have a long history and recently they have found application in several areas of AI, including belief revision and update, the representation of causal inferences in action planning and the formalization of hypothetical queries in deductive databases. Conditional logics have also been applied in order to formalize nonmonotonic reasoning. The study of the relations between conditional logics and nonmonotonic reasoning has led to the seminal work by Kraus, Lehmann and Magidor, who have introduced the so-called KLM framework. According to this framework, a defeasible knowledge base is represented by a finite set of conditional assertions of the form A |~ B, whose intuitive reading is ""typically (normally), the A's are B's"". The operator |~ is nonmonotonic in the sense that A |~ B does not imply A and C |~ B. The logics of the KLM framework, also known as preferential logics, allow to infer new conditional assertion from a given knowledge base. In spite of their significance, very few deductive mechanisms have been developed for conditional and preferential logics. In this book, the author tries to (partially) fill the existing gap by introducing proof methods (sequent and tableau calculi) for conditional and preferential logics, as well as theorem provers obtained by implementing the proposed calculi.

IOS Press is an international science, technical and medical publisher of high-quality books for academics, scientists, and professionals in all fields.

Some of the areas we publish in:

-Biomedicine -Oncology -Artificial intelligence -Databases and information systems -Maritime engineering -Nanotechnology -Geoengineering -All aspects of physics -E-governance -E-commerce -The knowledge economy -Urban studies -Arms control -Understanding and responding to terrorism -Medical informatics -Computer Sciences

Author(s): G.L. Pozzato
Series: Frontiers in Artificial Intelligence and Applications 208
Publisher: IOS Press
Year: 2010

Language: English
Pages: 209

Title page......Page 2
Preface......Page 6
Contents......Page 8
Introduction to Automated Reasoning - Monotonic vs Nonmonotonic Inference Systems......Page 10
Conditional Logics......Page 12
Preferential Logics......Page 13
Conditional Logics......Page 14
KLM Logics......Page 16
Proof Methods for Conditional Logics......Page 17
Proof Methods for Preferential Logics......Page 18
Theorem Provers......Page 19
Introduction......Page 20
Axiomatizations of Conditional Logics......Page 21
The Semantics of Conditional Logics......Page 23
The Selection Function Semantics......Page 24
The Sphere Semantics......Page 25
The Preference-Based Semantics......Page 26
Applications of Conditional Logics......Page 27
Nonmonotonic Reasoning......Page 29
The Solution of Kraus, Lehmann, and Magidor: the KLM Framework......Page 30
Rational Logic R......Page 32
Preferential Logic P......Page 36
Loop Cumulative Logic CL......Page 40
Cumulative Logic C......Page 45
Conditional Logics vs KLM Logics......Page 46
Introduction......Page 52
Recall to Conditional Logics......Page 53
A Sequent Calculus for Conditional Logics......Page 55
Basic Structural Properties of SeqS......Page 58
Soundness and Completeness of SeqS......Page 77
Decidability and Complexity......Page 80
Termination and Complexity for CK{+ID}{+MP}......Page 82
Termination and Complexity for CK+CEM{+ID}......Page 86
Termination and Complexity for CK+CS*......Page 88
Refinements and Other Properties for CK{+ID}{+MP}......Page 92
Refinements for CK{+ID}......Page 97
Uniform Proofs......Page 98
Examples in US'......Page 110
Conclusions......Page 113
Introduction......Page 114
A Tableau Calculus for Preferential Logic P......Page 116
Decidability and Complexity of P......Page 123
A Tableau Calculus for Loop Cumulative Logic CL......Page 131
Decidability and Complexity of CL......Page 136
A Tableau Calculus for Cumulative Logic C......Page 137
A Tableau Calculus for Rational Logic R......Page 153
Soundness, Termination, and Completeness of T R......Page 155
Complexity of R......Page 163
Conclusions and Comparison with Other Works......Page 165
Introduction......Page 167
CondLean: a Theorem Prover for Conditional Logics......Page 168
The Constant Labels Version......Page 169
The Free Variables Version......Page 171
CondLean's Graphical User Interface......Page 173
CondLean vs a "really-lean" Implementation......Page 175
GoalDUCK: a Goal-Directed Theorem Prover for Conditional Logics......Page 179
Statistics: CondLean and GoalDUCK......Page 181
KLMLean: a Theorem Prover for KLM Logics......Page 184
KLMLean for P and CL......Page 185
KLMLean for C......Page 186
KLMLean for R......Page 188
KLMLean's Graphical User Interface......Page 190
Performances of KLMLean......Page 192
Conclusions......Page 196
Future Work......Page 197
Application to the Description Logics......Page 198
Bibliography......Page 202