Order-sorted rewriting and congruence closure

José Meseguer

doi:10.1007/978-3-662-49630-5_29

Order-sorted rewriting and congruence closure

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

Abstract

Order-sorted type systems supporting inheritance hierarchies and subtype polymorphism are used in theorem proving, AI, and declarative programming. The satisfiability problems for the theories of: (i) order-sorted uninterpreted function symbols, and (ii) of such symbols modulo a subset Δ of associative-commutative ones are reduced to the unsorted versions of such problems at no extra computational cost. New results on order-sorted rewriting are needed to achieve this reduction.

Original language	English (US)
Title of host publication	Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings
Editors	Christof Löding, Bart Jacobs
Publisher	Springer
Pages	493-509
Number of pages	17
ISBN (Print)	9783662496299
DOIs	https://doi.org/10.1007/978-3-662-49630-5_29
State	Published - 2016
Event	19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016 - Eindhoven, Netherlands Duration: Apr 2 2016 → Apr 8 2016

Publication series

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

Other

Other	19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016
Country/Territory	Netherlands
City	Eindhoven
Period	4/2/16 → 4/8/16

Keywords

Congruence closure
Order-sorted rewriting
Satisfiability

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Online availability

10.1007/978-3-662-49630-5_29

Library availability

Discover UIUC Full Text

Cite this

Meseguer, J. (2016). Order-sorted rewriting and congruence closure. In C. Löding, & B. Jacobs (Eds.), Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings (pp. 493-509). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9634). Springer. https://doi.org/10.1007/978-3-662-49630-5_29

Order-sorted rewriting and congruence closure. / Meseguer, José.
Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings. ed. / Christof Löding; Bart Jacobs. Springer, 2016. p. 493-509 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9634).

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

Meseguer, J 2016, Order-sorted rewriting and congruence closure. in C Löding & B Jacobs (eds), Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9634, Springer, pp. 493-509, 19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, Netherlands, 4/2/16. https://doi.org/10.1007/978-3-662-49630-5_29

Meseguer J. Order-sorted rewriting and congruence closure. In Löding C, Jacobs B, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings. Springer. 2016. p. 493-509. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-662-49630-5_29

Meseguer, José. / Order-sorted rewriting and congruence closure. Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings. editor / Christof Löding ; Bart Jacobs. Springer, 2016. pp. 493-509 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{3e32e897d0e3481d87e33ee54b9ded22,

title = "Order-sorted rewriting and congruence closure",

abstract = "Order-sorted type systems supporting inheritance hierarchies and subtype polymorphism are used in theorem proving, AI, and declarative programming. The satisfiability problems for the theories of: (i) order-sorted uninterpreted function symbols, and (ii) of such symbols modulo a subset Δ of associative-commutative ones are reduced to the unsorted versions of such problems at no extra computational cost. New results on order-sorted rewriting are needed to achieve this reduction.",

keywords = "Congruence closure, Order-sorted rewriting, Satisfiability",

author = "Jos{\'e} Meseguer",

note = "Funding Information: Partially supported by NSF Grant CNS 13-19109. I thank Maria Paola Bonacina for suggested improvements. Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 2016.; 19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016 ; Conference date: 02-04-2016 Through 08-04-2016",

year = "2016",

doi = "10.1007/978-3-662-49630-5_29",

language = "English (US)",

isbn = "9783662496299",

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

publisher = "Springer",

pages = "493--509",

editor = "Christof L{\"o}ding and Bart Jacobs",

booktitle = "Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings",

address = "Germany",

}

TY - GEN

T1 - Order-sorted rewriting and congruence closure

AU - Meseguer, José

N1 - Funding Information: Partially supported by NSF Grant CNS 13-19109. I thank Maria Paola Bonacina for suggested improvements. Publisher Copyright: © Springer-Verlag Berlin Heidelberg 2016.

PY - 2016

Y1 - 2016

N2 - Order-sorted type systems supporting inheritance hierarchies and subtype polymorphism are used in theorem proving, AI, and declarative programming. The satisfiability problems for the theories of: (i) order-sorted uninterpreted function symbols, and (ii) of such symbols modulo a subset Δ of associative-commutative ones are reduced to the unsorted versions of such problems at no extra computational cost. New results on order-sorted rewriting are needed to achieve this reduction.

AB - Order-sorted type systems supporting inheritance hierarchies and subtype polymorphism are used in theorem proving, AI, and declarative programming. The satisfiability problems for the theories of: (i) order-sorted uninterpreted function symbols, and (ii) of such symbols modulo a subset Δ of associative-commutative ones are reduced to the unsorted versions of such problems at no extra computational cost. New results on order-sorted rewriting are needed to achieve this reduction.

KW - Congruence closure

KW - Order-sorted rewriting

KW - Satisfiability

UR - http://www.scopus.com/inward/record.url?scp=84961753567&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84961753567&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-49630-5_29

DO - 10.1007/978-3-662-49630-5_29

M3 - Conference contribution

AN - SCOPUS:84961753567

SN - 9783662496299

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

SP - 493

EP - 509

BT - Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Proceedings

A2 - Löding, Christof

A2 - Jacobs, Bart

PB - Springer

T2 - 19th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2016 and Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016

Y2 - 2 April 2016 through 8 April 2016

ER -

Order-sorted rewriting and congruence closure

Abstract

Publication series

Other

Keywords

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this