IWIL Accepted Papers with Abstracts

ABSTRACT. 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.

ABSTRACT. 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.

ABSTRACT. 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.

ABSTRACT. 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.