Zusammenfassung:
Die abhängige Typentheorie bietet ein ausdrucksstarkes Typensystem, das eine prägnante Formalisierung mathematischer Konzepte ermöglicht. In der Praxis wird sie hauptsächlich zum interaktiven Theorembeweisen mit intensionalen Typentheorien verwendet, wobei PVS eine bemerkenswerte Ausnahme darstellt. In diesem Beitrag stellen wir native Regeln für das automatisierte Schließen in einer abhängigkeitsbasierten Version (DHOL) der klassischen Logik höherer Ordnung (HOL) vor. DHOL hat eine erweiterbare Typentheorie mit einem unentscheidbaren Typprüfungsproblem, das Theorembeweise enthält. Wir haben die Inferenzregeln sowie einen automatischen Typüberprüfungsmodus in Lash implementiert, einem Fork von Satallax, dem führenden tableaux-basierten Beweiser für HOL. Unsere Methode ist solide und vollständig in Bezug auf die Beweisbarkeit in DHOL. Die Vollständigkeit wird durch die Einbindung einer soliden und vollständigen Übersetzung von DHOL nach HOL gewährleistet, die kürzlich von Rothgang et al. vorgeschlagen wurde. Darüber hinaus zeigen experimentelle Ergebnisse, dass die DHOL-Version von Lash alle wichtigen HOL-Prover, die mit der Übersetzung ausgeführt werden, übertreffen kann.