Order-sorted rewriting and congruence closure

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publicationFoundations 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
EditorsChristof Löding, Bart Jacobs
PublisherSpringer-Verlag Berlin Heidelberg
Pages493-509
Number of pages17
ISBN (Print)9783662496299
DOIs
StatePublished - Jan 1 2016
Event19th 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 2016Apr 8 2016

Publication series

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

Other

Other19th 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
CountryNetherlands
CityEindhoven
Period4/2/164/8/16

Keywords

  • Congruence closure
  • Order-sorted rewriting
  • Satisfiability

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Order-sorted rewriting and congruence closure'. Together they form a unique fingerprint.

  • 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-Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-662-49630-5_29