English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
  Superposition for Lambda-Free Higher-Order Logic

Bentkamp, A., Blanchette, J. C., Cruanes, S., & Waldmann, U. (2020). Superposition for Lambda-Free Higher-Order Logic. Retrieved from https://arxiv.org/abs/2005.02094.

Item is

Files

show Files
hide Files
:
arXiv:2005.02094.pdf (Preprint), 875KB
Name:
arXiv:2005.02094.pdf
Description:
File downloaded from arXiv at 2021-02-23 13:51
OA-Status:
Visibility:
Public
MIME-Type / Checksum:
application/pdf / [MD5]
Technical Metadata:
Copyright Date:
-
Copyright Info:
-

Locators

show

Creators

show
hide
 Creators:
Bentkamp, Alexander1, Author
Blanchette, Jasmin Christian1, Author           
Cruanes, Simon1, Author
Waldmann, Uwe2, Author           
Affiliations:
1External Organizations, ou_persistent22              
2Automation of Logic, MPI for Informatics, Max Planck Society, ou_1116545              

Content

show
hide
Free keywords: Computer Science, Logic in Computer Science, cs.LO,Computer Science, Artificial Intelligence, cs.AI
 Abstract: We introduce refutationally complete superposition calculi for intentional
and extensional clausal $\lambda$-free higher-order logic, two formalisms that
allow partial application and applied variables. The calculi are parameterized
by a term order that need not be fully monotonic, making it possible to employ
the $\lambda$-free higher-order lexicographic path and Knuth-Bendix orders. We
implemented the calculi in the Zipperposition prover and evaluated them on
Isabelle/HOL and TPTP benchmarks. They appear promising as a stepping stone
towards complete, highly efficient automatic theorem provers for full
higher-order logic.

Details

show
hide
Language(s): eng - English
 Dates: 2020-05-052021-02-202020
 Publication Status: Published online
 Pages: 37 p.
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: arXiv: 2005.02094
BibTex Citekey: Bentkamp2005.02094
URI: https://arxiv.org/abs/2005.02094
 Degree: -

Event

show

Legal Case

show

Project information

show

Source

show