Proof normalization modulo

Gilles Dowek; Benjamin Werner

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

Proof normalization modulo

Gilles Dowek
, Benjamin Werner

INRIA Rocquencourt

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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

Original language	English
Title of host publication	Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers
Editors	Thorsten Altenkirch, Bernhard Reus, Wolfgang Naraschewski
Publisher	Springer Verlag
Pages	62-77
Number of pages	16
ISBN (Print)	3540665374, 9783540665373
DOIs	https://doi.org/10.1007/3-540-48167-2_5
Publication status	Published - 1 Jan 1999
Externally published	Yes
Event	2nd International Workshop on Types for Proofs and Programs, TYPES 1998 - Kloster Irsee, Germany Duration: 27 Mar 1998 → 31 Mar 1998

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1657
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	2nd International Workshop on Types for Proofs and Programs, TYPES 1998
Country/Territory	Germany
City	Kloster Irsee
Period	27/03/98 → 31/03/98

Access to Document

10.1007/3-540-48167-2_5

Cite this

Dowek, G., & Werner, B. (1999). Proof normalization modulo. In T. Altenkirch, B. Reus, & W. Naraschewski (Eds.), Types for Proofs and Programs - International Workshop, TYPES 1998, Selected Papers (pp. 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. editor / Thorsten Altenkirch ; Bernhard Reus ; Wolfgang Naraschewski. Springer Verlag, 1999. pp. 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. in 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, pp. 62-77, 2nd International Workshop on Types for Proofs and Programs, TYPES 1998, Kloster Irsee, Germany, 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).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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. In Altenkirch T, Reus B, Naraschewski W, editors, 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

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this