Files in this item

FilesDescriptionFormat

application/pdf

application/pdfos-cong-clos.pdf (424kB)
(no description provided)PDF

Description

Title:Order-Sorted Rewriting and Congruence Closure
Author(s):Meseguer, José
Subject(s):order-sorted rewriting, congruence closure, satisfiability
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.
Issue Date:2015-06-04
Genre:Technical Report
Type:Text
Language:English
URI:http://hdl.handle.net/2142/78008
Sponsor:Partially supported by NSF Grant CNS 13-19109.
Date Available in IDEALS:2015-06-05


This item appears in the following Collection(s)

Item Statistics