Effective Higher-Order Automated Theorem Proving with integrated Descente Infinie and Presburger Arithmetic LEO-III

&

Abstract

This article has no associated abstract. (fix it)

Categories

Add categories

Keywords

Reprint years

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,150

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

My notes

Similar books and articles

Equality and Extensionality in Higher-Order Theorem Proving.Benzmüller Christoph - 1999 - Dissertation, Naturwissenschaftlich-Technische Fakultät I, Saarland University, Saarbrücken, Germany
The Higher-Order Prover LEO-II.Christoph Benzmüller, Nik Sultana, Lawrence C. Paulson & Frank Theiß - 2015 - Journal of Automated Reasoning 55 (4):389-404.
System description: { A higher-order theorem prover?Michael Kohlhase - manuscript
Higher-Order Automated Theorem Provers.Benzmüller Christoph - 2015 - In David Delahaye & Bruno Woltzenlogel Paleo (eds.), All About Proofs, Proof for All. College Publications. pp. 171-214.
Descente Infinie + Deduction.Claus-Peter Wirth - 2004 - Logic Journal of the IGPL 12 (1):1-96.
Automated reasoning in higher-order logic using the tptp thf infrastructure.Sutcliffe Geoff & Benzmüller Christoph - 2010 - Journal of Formalized Reasoning 3 (1):1-27.
Combined reasoning by automated cooperation.Christoph Benzmüller, Volker Sorge, Mateja Jamnik & Manfred Kerber - 2008 - Journal of Applied Logic 6 (3):318-342.
LEO-II im Ontologieschliessen -- Antrag auf ein Forschungsvorhaben an die DFG.Benzmüller Christoph - 2009
Cumulative Habilitation Script.Christoph Benzmüller - 2006 - Saarland University, Germany.
Higher-order automated theorem proving.Michael Kohlhase - unknown
Multimodal and intuitionistic logics in simple type theory.Christoph Benzmueller & Lawrence Paulson - 2010 - Logic Journal of the IGPL 18 (6):881-892.
Gödel’s God in Isabelle/HOL.Benzmüller Christoph & Woltzenlogel Paleo Bruno - 2013 - Archive of Formal Proofs.
Higher-order Aspects and Context in SUMO.Christoph Benzmüller & Adam Pease - 2012 - Journal of Web Semantics 12:104-117.
Connection Tableau Calculi with Disjunctive Constraints.Ortrun Ibens - 2002 - Studia Logica 70 (2):241-270.
Connection tableau calculi with disjunctive constraints.Ortrun Ibens - 2002 - Studia Logica 70 (2):241 - 270.

Analytics

Added to PP
2017-12-04

Downloads
0

6 months
0

Historical graph of downloads

Sorry, there are not enough data points to plot this chart.
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references