Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

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:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-91-218.pdfMPI-I-91-218.pdfMPI-I-91-218.dvi276 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
Hide details for BibTeXBibTeX
@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},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-91-218},
  MONTH = {December},
  YEAR = {1991},
  ISSN = {0946-011X},
}