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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
os-cong-clos.pdf
