MPI-INF/SWS Research Reports 1991-2017

2. Number - only D2


A sorted logic using dynamic sorts

Weidenbach, Christoph

December 1991, 71 pages.

Status: available - back from printing

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.

  • MPI-I-91-218.pdfMPI-I-91-218.pdfMPI-I-91-218.dvi
  • Attachement: MPI-I-91-218.dvi (276 KBytes); MPI-I-91-218.pdf (304 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  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},