Autologic

Autologic : Proof Theory and Automated Deduction

By (author) 

List price: US$72.00

Currently unavailable

Add to wishlist

AbeBooks may have this title (opens in new window).

Try AbeBooks

Description

This book has evolved from the author's theory that if it is possible to teach students reasonable methods for finding proofs (in a system of natural deduction), then it should also be possible to express those methods in a programming language, and program on a computer the effective skills taught in logic courses. He rejected classical logic and, in his book "Anti-realism and Logic", gave arguments in favour of a system he called "intuitionistic relevant logic". He found that working within that system he could find proofs more easily because of the constraint of relevance between their premisses and their conclusions. A report on natural deduction based sub-classical computational logic, this book should be of interest to computational logicians, proof theorists, cognitive scientists, workers in artificial intelligence and the Prolog and logic programming community.show more

Product details

  • Hardback | 256 pages
  • 144.78 x 215.9 x 22.86mm | 453.59g
  • EDINBURGH UNIVERSITY PRESS
  • Edinburgh, United Kingdom
  • English
  • bibliography, glossary, index
  • 0748603581
  • 9780748603589

Table of contents

Computational logic and Prolog, three well-known systems of logic, computational logic and complexity, the choice of minimal logic, relevance; the relevance of relevance - complexity considerations, the design of expert systems, relevantizing mathematics, a clash of paradigms; logic and cognitive science - on inference engines, methodological choices, emulation by simulation, computational logic and proof theory, compossible constraints, "my program is better than your program"; from Oracles to Rationauts; minimal logic in perspective; exploring the rules; how does one search for proofs?; accessibility and relevance - accessibility, relevance, proof by cases; genetic screening in IR; how to represemt formulae; how to represent proofs; how to generate proofs; features of a natural proof-finder; on avoiding loops and blind alleys - the Dyckhoff device, fettering, hobbling, tethering; proof theory and proof search - vindication of a proof-theoretic approach, testing proof-finders, looking ahead to IR; summary of proof-theoretic results; deductive debuggers for minimal logic; Pellitier's propositional problems; the associativity problems; some simple Prolog proof-finders.show more