Completion and Equational Theorem Proving using Taxonomic Constraints

  • We present an approach to prove several theorems in slightly different axiomsystems simultaneously. We represent the different problems as a taxonomy, i.e.a tree in which each node inherits all knowledge of its predecessors, and solve theproblems using inference steps on rules and equations with simple constraints,i.e. words identifying nodes in the taxonomy. We demonstrate that a substantialgain can be achieved by using taxonomic constraints, not only by avoiding therepetition of inference steps in the different problems but also by achieving runtimes that are much shorter than the accumulated run times when proving eachproblem separately.

Metadaten exportieren

  • Export nach Bibtex
  • Export nach RIS

Weitere Dienste

Teilen auf Twitter Suche bei Google Scholar
Metadaten
Verfasserangaben:Jörg Denzinger
URN (Permalink):urn:nbn:de:hbz:386-kluedo-3528
Schriftenreihe (Bandnummer):SEKI Report (95,11)
Dokumentart:Preprint
Sprache der Veröffentlichung:Englisch
Jahr der Fertigstellung:1999
Jahr der Veröffentlichung:1999
Veröffentlichende Institution:Technische Universität Kaiserslautern
Datum der Publikation (Server):03.04.2000
Fachbereiche / Organisatorische Einheiten:Fachbereich Informatik
DDC-Sachgruppen:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik
Lizenz (Deutsch):Standard gemäß KLUEDO-Leitlinien vor dem 27.05.2011

$Rev: 13581 $