Proof normalization modulo

Gilles Dowek; Benjamin Werner

doi:10.1007/3-540-48167-2_5

Proof normalization modulo

Gilles Dowek
, Benjamin Werner

INRIA Rocquencourt

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

We consider a class of logical formalisms, in which first-order logic is extended by identifying propositions modulo a given congruence. We particularly focus on the case where this congruence is induced by a confluent and terminating rewrite system over the propositions. We show that this extension enhances the power of first-order logic and that various formalisms, including Church’s higher-order logic (HOL) can be described in our framework. We conjecture that proof normalization and logical consistency always hold over this class of formalisms, provided some minimal conditions over the rewrite system are fulfilled. We prove this conjecture for some subcases, including HOL.

langue originale	Anglais
titre	Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers
rédacteurs en chef	Thorsten Altenkirch, Bernhard Reus, Wolfgang Naraschewski
Editeur	Springer Verlag
Pages	62-77
Nombre de pages	16
ISBN (imprimé)	3540665374, 9783540665373
Les DOIs	https://doi.org/10.1007/3-540-48167-2_5
état	Publié - 1 janv. 1999
Modification externe	Oui
Evénement	2nd International Workshop on Types for Proofs and Programs, TYPES 1998 - Kloster Irsee, Allemagne Durée: 27 mars 1998 → 31 mars 1998

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1657
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	2nd International Workshop on Types for Proofs and Programs, TYPES 1998
Pays/Territoire	Allemagne
La ville	Kloster Irsee
période	27/03/98 → 31/03/98

Accès au document

10.1007/3-540-48167-2_5

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

Dowek, G., & Werner, B. (1999). Proof normalization modulo. Dans T. Altenkirch, B. Reus, & W. Naraschewski (eds.), Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers (p. 62-77). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 1657). Springer Verlag. https://doi.org/10.1007/3-540-48167-2_5

Dowek, Gilles ; Werner, Benjamin. / Proof normalization modulo. Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers. Editeur / Thorsten Altenkirch ; Bernhard Reus ; Wolfgang Naraschewski. Springer Verlag, 1999. p. 62-77 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{2bec9f7aba51420eb90ff7f75c68db1d,

title = "Proof normalization modulo",

abstract = "We consider a class of logical formalisms, in which first-order logic is extended by identifying propositions modulo a given congruence. We particularly focus on the case where this congruence is induced by a confluent and terminating rewrite system over the propositions. We show that this extension enhances the power of first-order logic and that various formalisms, including Church{\textquoteright}s higher-order logic (HOL) can be described in our framework. We conjecture that proof normalization and logical consistency always hold over this class of formalisms, provided some minimal conditions over the rewrite system are fulfilled. We prove this conjecture for some subcases, including HOL.",

author = "Gilles Dowek and Benjamin Werner",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1999.; 2nd International Workshop on Types for Proofs and Programs, TYPES 1998 ; Conference date: 27-03-1998 Through 31-03-1998",

year = "1999",

month = jan,

day = "1",

doi = "10.1007/3-540-48167-2\_5",

language = "English",

isbn = "3540665374",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "62--77",

editor = "Thorsten Altenkirch and Bernhard Reus and Wolfgang Naraschewski",

booktitle = "Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers",

}

Dowek, G & Werner, B 1999, Proof normalization modulo. Dans T Altenkirch, B Reus & W Naraschewski (eds), Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), VOL. 1657, Springer Verlag, p. 62-77, 2nd International Workshop on Types for Proofs and Programs, TYPES 1998, Kloster Irsee, Allemagne, 27/03/98. https://doi.org/10.1007/3-540-48167-2_5

Proof normalization modulo. / Dowek, Gilles; Werner, Benjamin.
Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers. Ed. / Thorsten Altenkirch; Bernhard Reus; Wolfgang Naraschewski. Springer Verlag, 1999. p. 62-77 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 1657).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

TY - GEN

T1 - Proof normalization modulo

AU - Dowek, Gilles

AU - Werner, Benjamin

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1999.

PY - 1999/1/1

Y1 - 1999/1/1

N2 - We consider a class of logical formalisms, in which first-order logic is extended by identifying propositions modulo a given congruence. We particularly focus on the case where this congruence is induced by a confluent and terminating rewrite system over the propositions. We show that this extension enhances the power of first-order logic and that various formalisms, including Church’s higher-order logic (HOL) can be described in our framework. We conjecture that proof normalization and logical consistency always hold over this class of formalisms, provided some minimal conditions over the rewrite system are fulfilled. We prove this conjecture for some subcases, including HOL.

AB - We consider a class of logical formalisms, in which first-order logic is extended by identifying propositions modulo a given congruence. We particularly focus on the case where this congruence is induced by a confluent and terminating rewrite system over the propositions. We show that this extension enhances the power of first-order logic and that various formalisms, including Church’s higher-order logic (HOL) can be described in our framework. We conjecture that proof normalization and logical consistency always hold over this class of formalisms, provided some minimal conditions over the rewrite system are fulfilled. We prove this conjecture for some subcases, including HOL.

UR - https://www.scopus.com/pages/publications/84957029977

U2 - 10.1007/3-540-48167-2_5

DO - 10.1007/3-540-48167-2_5

M3 - Conference contribution

AN - SCOPUS:84957029977

SN - 3540665374

SN - 9783540665373

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 62

EP - 77

BT - Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers

A2 - Altenkirch, Thorsten

A2 - Reus, Bernhard

A2 - Naraschewski, Wolfgang

PB - Springer Verlag

T2 - 2nd International Workshop on Types for Proofs and Programs, TYPES 1998

Y2 - 27 March 1998 through 31 March 1998

ER -

Dowek G, Werner B. Proof normalization modulo. Dans Altenkirch T, Reus B, Naraschewski W, rédacteurs en chef, Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers. Springer Verlag. 1999. p. 62-77. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-48167-2_5

Proof normalization modulo

Résumé

Série de publications

Une conférence

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation