دانلود کتاب Automated Proof Search in Non-Classical Logics: Efficient Matrix Proof Methods for Modal and Intuitionistic Logics [PhD Thesis]

This book is a revised version of my PhD. dissertation submitted to the Dept. of Artificial Intelligence, University of Edinburgh, Scotland, under the supervision of Prof. Alan Bundy.Although Leibniz' seventeenth-century dream of a symbolic language for the representation and mechanical solution of all scientific and mathematical problems has suffered at the hands of the undecidability, incompleteness and independence results of modern mathematical logic, the spirit of his idea lives on within Computing Science. It has proved practical to solve problems mechanically by testing sentences of a symbolic logic for theoremhood using a computer, even though the decision problem for the logic might be technically intractable. The practical performance of algorithms for such automated deduction — or automated proof search — can be improved by standard optimisation techniques, novel data structures and more powerful hardware, but in the final analysis successful algorithms arise from computationally sensitive characterisations of the logics themselves.In this book a number of such computationally sensitive characterisations are developed for various first-order logics. The aim has been to lay the groundwork for a theory of automated deduction in arbitrary symbolic logics by providing empirical evidence for the existence of a uniform approach to efficient proof search in both truth-functional and non truth-functional logics.