IWIL ON SATURDAY, DECEMBER 14TH, 2013

Most input languages for ATP systems, including the existing TPTP language, are designed primarily to write the logical formulae that are input to the ATP systems' reasoning processes. There is minimal or no support for controlling the processing of the logical formulae: tasks such as incrementally adding and deleting formulae, controlling reasoning processes, and interacting with non-logical data. The TPTP Process Instruction (TPI) language augments the existing and well-known logical TPTP language forms with command and control instructions for manipulating logical formulae in the context of ATP systems. The TPI language makes it easy(er) for ATP users to specify their problems, process the logical formulae, and report results, in a fully automatic way.

Attempts to prove the existence (or non-existence) of God by means of abstract ontological arguments are an old tradition in philosophy and theology. 

 We have analyzed Dana Scott’s version of Goedel’s proof for the first-time with an unprecedented degree of detail and formality with the help of higher-order theorem provers; cf. https://github.com/ FormalTheology/GoedelGod. Our computer-assisted formalizations rely on an embedding of quantified modal logic into classical higher-order logic with Henkin semantics.

The following has been done (and in this order): (i) a detailed natural deduction proof; (ii) a formalization in TPTP THF syntax; (iii) an automatic verification of the consistency of the axioms and definitions with Nitpick; (iv) an automatic demonstration of the theorems with the provers LEO-II and Satallax; (v) a step-by-step formalization using the Coq proof assistant; (vi) a formalization using the Isabelle proof assistant, where the theorems have been automated with the Isabelle tools Sledgehammer and Metis. Furthermore, the multi-step THF development of the proof has recently been encoded in Sutcliffe’s new TPTP TPI scripting language. This scripting language offers important features that were missing in the TPTP world so far. 

In our ongoing computer-assisted study of G ̈odel’s proof, the automated reasoning tools have made some interesting observations, some of which were unknown so far. Our work attests the maturity of contemporary interactive and automated deduction tools for classical higher-order logic and demonstrates the elegance and practical relevance of the embeddings-based approach. Most importantly, our work opens new perspectives for a computer-assisted theoretical philosophy. 

In this paper we present an interactive prover for deciding formulas in propositional bi-intuitionistic logic (BiInt). This tool is based on a recent connection-based characterization of bi-intuitionistic validity through bi-intuitionistic resource graphs (biRG). After giving the main concepts and principles we illustrate how to use this interactive proof or counter-model building assistant and emphasize the interest of bi- intuitionistic resource graphs for proving or refuting BiInt formulas. We complete this work by studying how to make our tool a fully automated theorem prover.

This paper provides a new presentation of the lambda-pi calculus modulo where the addition of rewrite rules is made explicit. The lambda-pi calculus modulo is a variant of the lambda calculus with dependent types where beta-reduction is extended with user-defined rewrite rules. Its expressiveness makes it suitable to serve as an output language for theorem provers, certified development tools or proof assistants. Addition of rewrite rules becomes an iterative process and rules previously added can be used to type new rules. We also discuss the condition rewrite rules must satisfy in order to preserve the Subject Reduction property and we give a criterion weaker than the usual one. Finally we describe the new version of Dedukti, a type-checker for the lambda-pi calculus modulo for which we assess its efficiency in comparison with Coq Twelf and Maude.

We present the certifying part of the Zenon Modulo automated theorem prover, which is an extension of the Zenon tableau-based first order automated theorem prover to deduction modulo. The theory of deduction modulo is an extension of predicate calculus, which allows us to rewrite terms as well as propositions, and which is well suited for proof search in axiomatic theories, as it turns axioms into rewrite rules. In addition, deduction modulo allows Zenon Modulo to compress proofs by making computations implicit in proofs. To certify these proofs, we use Dedukti, an external proof checker for the lambda-Pi-calculus modulo, which can deal natively with proofs in deduction modulo. To assess our approach, we rely on some experimental results obtained on the benchmarks provided by the TPTP library.