In this thesis we develop efficient methods for automated proof search within an important class of mathematical logics. The logics considered are the varying, cumulative and constant domain versions of the first-order modal logics K, K4, D, D4, T, S4 and S5, and first-order intuitionistic logic. The use of these non-classical logics is commonplace within Computing Science and Artificial Intelligence in applications in which efficient machine assisted proof search is essential. Traditional techniques for the design of efficient proof methods for classical logic prove to be of limited use in this context due to their dependence on properties of classical logic not shared by most of the logics under consideration. One major contribution of this thesis is to reformulate and abstract some of these classical techniques to facilitate their application to a wider class of mathematical logics. We begin with Bibel's Connection Calculus: a matrix proof method for classical logic comparable in efficiency with most machine orientated proof methods for that logic. We reformulate this method to support its decomposition into a collection of individual techniques for improving the efficiency of proof search within a standard cut-free sequent calculus for classical logic. Each technique is presented as a means of alleviating a particular form of redundancy manifest within sequent-based proof search. One important result that arises from this anaylsis is an appreciation of the role of unification as a tool for removing certain proof-theoretic complexities of specific sequent rules; in the case of classical logic: the interaction of the quantifier rules. All of the non-classical logics under consideration admit complete sequent calculi. We anaylse the search spaces induced by these sequent proof systems and apply the techniques identified previously to remove specific redundancies found therein. Significantly, our proof-theoretic analysis of the role of unification renders it useful even within the propositional fragments of modal and intuitionistic logic.

Systems code is almost universally written in the C programming language or a variant. C has a very low level of type and memory abstraction and formal reasoning about C systems code requires a memory model that is able to capture the semantics of C pointers and types. At the same time, proof-based verification demands abstraction, in particular from the aliasing and frame problems. In this thesis, we study the mechanisation of a series of models, from semantic to separation logic, for achieving this abstraction when performing interactive theorem-prover based verification of C systems code in higher- order logic. We do not commit common oversimplifications, but correctly deal with C's model of programming language values and the heap, while developing the ability to reason abstractly and efficiently. We validate our work by demonstrating that the models are applicable to real, security- and safety-critical code by formally verifying the memory allocator of the L4 microkernel. All formalisations and proofs have been developed and machine-checked in the Isabelle/HOL theorem prover.

Modal logics have found applications in many diferent contexts. For example, epistemic modal logics can be used to reason about security protocols, temporal modal logics can be used to reason about the correctness of distributed systems and propositional dynamic logic can reason about the correctness of programs. However, pure modal logic is expressively weak and cannot represent many interesting secondorder properties that are expressible, for example, in the μ-calculus. Here we investigate the extension of modal logics with propositional quantification modulo bisimulation (bisimulation quantification). We extend existing work on bisimulation quantified modal logic by considering the variety of logics that result by restricting the structures over which they are interpreted. We show this can be a natural extension of modal logic preserving the intuitions of both modal logic and propositional quantification. However, we also find cases where such intuitions are not preserved. We examine cases where the axioms of pure modal logic and propositional quantification are preserved and where bisimulation quantifiers preserve the decidability of modal logic. We translate a number of recent decidability results for monadic second-order logics into the context of bisimulation quantified modal logics, and show how these results can be used to generate a number of interesting bisimulation quantified modal logics.

Thesis (Dr. rer. nat.)--Technische Universität München, 2000. / "Infix"--Cover. Includes bibliographical references (p. [164]-175) and index.

Univ., Diss.--Cambridge, 1991. / Literaturverz. S. [133] - 138.

Thesis (Ph.D.) - University of Queensland, 2006. / Includes bibliography.

Τα «Συστήματα Αυτόματης Απόδειξης Θεωρημάτων-ΣΑΑΘ» (Automatic Theorem Proving Systems-ATP Systems) είναι συστήματα βασισμένα στη λογική πρώτης τάξεως, τα οποία μπορούν από ένα σύνολο λογικών προτάσεων να συνάγουν την αλήθεια μιας δεδομένης λογικής πρότασης με αυτόματο τρόπο. Η διαδικασία της απόδειξης στα περισσότερα ΣΑΑΘ στηρίζεται στην αρχή της επίλυσης, τον ισχυρότερο κανόνα λογικής εξαγωγής συμπερασμάτων, και την αντίφαση της επίλυσης, μια διαδικασία που εξασφαλίζει την ορθότητα των συμπερασμάτων. Ο ACT-P είναι ένα ΣΑΑΘ που στηρίζεται στην αρχή της επίλυσης και την αντίφαση της επίλυσης, γραμμένο στο εργαλείο GCLISP Developer 5.0 της Gold-Hill, και διαθέτει μια βιβλιοθήκη γνωστών στρατηγικών ελέγχου της διαδικασίας απόδειξης, προσφέροντας τη δυνατότητα στον χρήστη να ορίσει κάθε φορά ένα (κατάλληλο) συνδυασμό στρατηγικών. Στην εργασία αυτή έγινε κατ’ αρχήν μεταφορά του ACT-P σε LispWorks, ένα δυναμικότερο εργαλείο ανάπτυξης εφαρμογών σε Lisp. Επιπλέον, ο χρήστης μέσω του νέου παραθυρικού περιβάλλοντος μπορεί να βλέπει δυο διαφορετικές λύσεις του ίδιου προβλήματος, τη συνοπτική και αναλυτική λύση. Στη συνέχεια, έγινε έλεγχος της καλής λειτουργίας του ACT-P και των στρατηγικών του μέσω δοκιμών με προβλήματα που προέρχονται από την TPTP (Thousands of Problems for Theorem Provers), μια γνωστή βιβλιοθήκη προβλημάτων για ΣΣΑΘ συστήματα στο Διαδίκτυο, και έγιναν οι απαραίτητες διορθώσεις έτσι ώστε να επιλύει προβλήματα από διάφορες κατηγορίες προβλημάτων της βιβλιοθήκης TPTP. Τέλος, έγινε μια μελέτη χρήσης διαφόρων συνδυασμών στρατηγικών ελέγχου για διάφορα προβλήματα της TPTP και εξήχθησαν χρήσιμα συμπεράσματα για την καταλληλότητά τους και την αποδοτικότητά τους σε σχέση με το είδος των προβλημάτων. / Automatic Theorem Proving Systems (ATP Systems) are based on First Order Logic (FOL) and are able to automatically prove the truth of logical sentence. The proof procedure in most ATP Systems uses the resolution principle which is the strongest existing inference rule, and the resolution refutation process which ensure soundeness of the conclusion. The ACT-P is an ATP System which uses the resolution principle and the resolution refutation and it is written in GCLISP Developer 5.0 of Gold-Hill. ACT-P has a library of strategies to control the proof process, and gives users the ability to assign to specify a suitable combination of strategies. In this dissertation a new window based interface is developed for ACTP in Lispworks, which is a powerful tool for developing Lisp applications. The interface gives to the user a more thorough view of the solving process. Moreover, the user can see two different solutions of the problem, the brief and the analytic one. In addition, the functionality and the strategies of ACTP were tested on problems from the TPTP (Thousands of Problems for Theorem Provers) which is a known library of problems for ATP Systems on the web. ACTP has been improved so as to solve problems from various categories of the TPTP library. Finally, different strategy combinations for solving problems from various categories of TPTP library were studied, leading to useful conclusions about the suitability and the performance of the different combinations depending on the problems.

- / -

Capes / A partir dos teoremas encontrados na publicação Geometriae Pars Universalis de 1668 são apresentadas, pela primeira vez em português, as demonstrações dos teoremas de Pappus para os sólidos de revolução. Essa publicação, escrita originalmente em latim, foi feita pelo matemático escocês James Gregory (1638-1675) e é anterior ao desenvolvimento do Cálculo. Além disso, alguns conceitos de Cálculo e de centro de gravidade são revistos a fim de também apresentarumademonstraçãodessesteoremasapartirdessasferramentas. Ainda são feitas algumas aplicações dos teoremas de Pappus para os casos diretos, onde o eixo de rotação ou revolução é representado por um dos eixos coordenados ou ainda, por uma reta paralela a eles. Também são mostrados casos onde o eixo de rotação é dado por uma reta inclinada no plano cartesiano, deixando claro a abrangência, eficiência e a relativa simplicidade de aplicação desses teoremas. / From the theorems found in the publication Geometriae Pars Universalisof 1668 are presented, for the first time in portuguese, the proof of Pappus’s theorems for solids of revolution. This publication , originally written in latin, is due to the scottish mathematician James Gregory (1638-1675) and is prior to the development of Calculus. Furthermore some concepts of Calculus and center of gravity are also revised to present a proof of these theorems from these tools. Some direct cases for Pappus’s theorems are presented, where the axis of rotation or revolution is represented by one of the coordinate axes or by a straight line parallel to them. Also shown are cases where the axis of rotation is given by a straight tilted in the cartesian plane, showing the scope, efficiency and relative simplicity of applying these theorems.

The thesis describes a rational reconstruction of Sowa's theory of Conceptual Graphs. The reconstruction produces a theory with a firmer logical foundation than was previously the case and which is suitable for computation whilst retaining the expressiveness of the original theory. Also, several areas of incompleteness are addressed. These mainly concern the scope of operations on conceptual graphs of different types but include extensions for logics of higher orders than first order. An important innovation is the placing of negation onto a sound representational basis. A comparison of theorem proving techniques is made from which the principles of theorem proving in Peirce logic are identified. As a result, a set of derived inference rules, suitable for a goal driven approach to theorem proving, is developed from Peirce's beta rules. These derived rules, the first of their kind for Peirce logic and conceptual graphs, allow the development of a novel theorem proving approach which has some similarities to a combined semantic tableau and resolution methodology. With this methodology it is shown that a logically complete yet tractable system is possible. An important result is the identification of domain independent heuristics which follow directly from the methodology. In addition to the theorem prover, an efficient system for the detection of selectional constraint violations is developed. The proof techniques are used to build a working knowledge base system in Prolog which can accept arbitrary statements represented by conceptual graphs and test their semantic and logical consistency against a dynamic knowledge base. The same proof techniques are used to find solutions to arbitrary queries. Since the system is logically complete it can maintain the integrity of its knowledge base and answer queries in a fully automated manner. Thus the system is completely declarative and does not require any programming whatever by a user with the result that all interaction with a user is conversational. Finally, the system is compared with other theorem proving systems which are based upon Conceptual Graphs and conclusions about the effectiveness of the methodology are drawn.