English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 DetailsSummary
  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

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/21.11116/0000-0008-0A5F-4 Version Permalink: https://hdl.handle.net/21.11116/0000-0008-0A60-1
Genre: Paper

Files

show Files
hide Files
:
arXiv:2005.02094.pdf (Preprint), 875KB
View   Save
File Permalink:
https://hdl.handle.net/21.11116/0000-0008-0A61-0
Name:
arXiv:2005.02094.pdf
Description:
File downloaded from arXiv at 2021-02-23 13:51
OA-Status:
Not specified
Visibility:
Public
MIME-Type / Checksum:
application/pdf / [MD5]
Technical Metadata:
View
Copyright Date:
-
Copyright Info:
-
License:
http://arxiv.org/licenses/nonexclusive-distrib/1.0/

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