Automated Deduction in Classical and Non-Classical Logics Select
- PDF / 4,739,126 Bytes
- 306 Pages / 446.727 x 680.671 pts Page_size
- 75 Downloads / 207 Views
Lecture Notes in Computer Science Edited by G. Goos, J. Hartmanis and J. van Leeuwen
1761
3 Berlin Heidelberg New York Barcelona Hong Kong London Milan Paris Singapore Tokyo
Ricardo Caferra Gernot Salzer (Eds.)
Automated Deduction in Classical and Non-Classical Logics Selected Papers
13
Series Editors Jaime G. Carbonell, Carnegie Mellon University, Pittsburgh, PA, USA J¨org Siekmann, University of Saarland, Saarbr¨ucken, Germany Volume Editors Ricardo Caferra Leibniz-IMAG 46 Avenue Felix Viallet, 38031 Grenoble cedex, France E-mail: [email protected] Gernot Salzer Technical University of Vienna Favoritenstraße 9-11/E185-2, 1040 Vienna, Austria E-mail: [email protected]
Cataloging-in-Publication data applied for Die Deutsche Bibliothek - CIP-Einheitsaufnahme Automated deduction in classical and non-classical logics / Ricardo Caferra ; Gernot Salzer (ed.). - Berlin ; Heidelberg ; New York ; Barcelona ; Hong Kong ; London ; Milan ; Paris ; Singapore ; Tokyo : Springer, 2000 (Lecture notes in computer science ; Vol. 1761 : Lecture notes in artificial intelligence) ISBN 3-540-67190-0
CR Subject Classification (1998): I.2.3, F.4.1, F.3.1
ISSN 0302-9743 ISBN 3-540-67190-0 Springer-Verlag Berlin Heidelberg New York This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically the rights of translation, reprinting, re-use of illustrations, recitation, broadcasting, reproduction on microfilms or in any other way, and storage in data banks. Duplication of this publication or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965, in its current version, and permission for use must always be obtained from Springer-Verlag. Violations are liable for prosecution under the German Copyright Law. Springer-Verlag is a company in the specialist publishing group BertelsmannSpringer c Springer-Verlag Berlin Heidelberg 2000 Printed in Germany Typesetting: Camera-ready by author Printed on acid-free paper SPIN 10719651
06/3142
543210
Preface
This volume is a collection of papers on automated deduction in classical, modal, and many-valued logics, with an emphasis on first-order theories. Some authors bridge the gap to higher-order logic by dealing with simple type theory in a firstorder setting, or by resolving shortcomings of first-order logic with the help of higher-order notions. Most papers rely on resolution or tableaux methods, with a few exceptions choosing the equational paradigm. In its entirety the volume is a mirror of contemporary research in first-order theorem proving. One trend to be observed is the interest in effective decision procedures. The main aim of first-order theorem proving was and still is to demonstrate the validity or unsatisfiability of formulas, by more and more sophisticated methods. Within the last years, however, the other side of the medal – falsifiability and satisfiability – has received growing attention. Though in general non-terminating, theorem provers sometimes act as deci
Data Loading...
