max planck institut
informatik

# MPI-I-91-218

## A sorted logic using dynamic sorts

### Weidenbach, Christoph

MPI-I-91-218. December 1991, 71 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
We present a sound and complete calculus $\cal {CL}_S$ for the first-order logic ${\cal L_S}$ without equality but dynamic sorts. By dynamic sorts we understand a sort structure which is exploited during the deduction process and is not fixed from the beginning. Therefore the logic allows arbitrary sort declarations and every first-order logic formula can be compiled into our logic. Deductions in the calculus turn out to be very efficient as will be shown by examples. Thus the new logic signifacantly improves the efficiency of automated deductions if one-place predicates (sorts) are involved in the reasoning process. Furthermore the calculus $\cal {CL}_S$ is conservative extension of the existing approaches to sorted logic. That means if the sorted information could be represented in the known approaches the more general calculus $\cal {CL}_S$ has the same behaviour as the existing calculi.
Acknowledgement:
References to related material:

MPI-I-91-218.pdf276 KBytes; 304 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1991-218
BibTeX
@TECHREPORT{Weidenbach-91-mpii218,
AUTHOR = {Weidenbach, Christoph},
TITLE = {A sorted logic using dynamic sorts},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},