A Simple Deduction System for First-Order Logic with Equality, Free Constructors and Induction

Abstract : Proof systems like Coq feature inductive datatypes, where datatype constructor- s are free in the sense that two terms built from constructors only are semantically equal if and only if they are syntactically identical. Although free constructors are an essential ingredient of modern formalized mathematics- , no automated first-order prover has been specialized with built-in rules for dealing with free constructors, until now. We propose a sequent system for a logic where terms can be built only from variables and free constructors- . Thus the logic will be kept simple, as equality in the logic will be syntactical equality. We show how partial functions can be introduced into the logic, in the form of predicates obeying some functionality constrain- ts. We prove that the resulting system is sound and complete with respect to a natural first-order semantics of datatypes, and enjoys cut elimination. We then develop a tableau calculus to find proofs in this sequent system. This involves solving an extended form of unification, which unfortunately is undecidable: we show that it indeed includes second-order predicate unification as a subproblem. Nonetheless, we describe a non-terminating procedure to solve such unification problems, and give a few hints so as to improve its efficiency in practice. Finally, we extend the system to include first-order structural induction principles on datatype values. This does not pose any difficulty, apart from the expected problem of induction loading-namely, that we may need to generalize a proposition before we can prove it by induction.
Type de document :
Rapport
[Research Report] RR-3653, INRIA. 1999
Liste complète des métadonnées

https://hal.inria.fr/inria-00073019
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 11:36:56
Dernière modification le : vendredi 1 juin 2018 - 12:02:02
Document(s) archivé(s) le : dimanche 4 avril 2010 - 23:31:29

Fichiers

Identifiants

  • HAL Id : inria-00073019, version 1

Collections

Citation

Jean Goubault-Larrecq. A Simple Deduction System for First-Order Logic with Equality, Free Constructors and Induction. [Research Report] RR-3653, INRIA. 1999. 〈inria-00073019〉

Partager

Métriques

Consultations de la notice

199

Téléchargements de fichiers

126