English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
 
 
DownloadE-Mail
 Local TagsRelease HistoryDetailsSummary
  Superposition with Lambdas

Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P., & Waldmann, U. (2021). Superposition with Lambdas. Retrieved from https://arxiv.org/abs/2102.00453.

Item is

 

show all hide all

Basic

show hide
Item Permalink: https://hdl.handle.net/21.11116/0000-0008-0A44-1 Version Permalink: https://hdl.handle.net/21.11116/0000-000E-3455-8
Genre: Paper

Files

show Files
hide Files
:
arXiv:2102.00453.pdf (Preprint), 500KB
View   Save
File Permalink:
https://hdl.handle.net/21.11116/0000-0008-0A46-F
Name:
arXiv:2102.00453.pdf
Description:
File downloaded from arXiv at 2021-02-23 13:31
OA-Status:
Not specified
Visibility:
Public
MIME-Type / Checksum:
application/pdf / [MD5]
Technical Metadata:
View
Copyright Date:
-
Copyright Info:
-
License:
http://creativecommons.org/licenses/by/4.0/

Locators

show

Creators

show
hide
 Creators:
Bentkamp, Alexander1, Author
Blanchette, Jasmin2, Author           
Tourret, Sophie2, Author           
Vukmirović, Petar1, 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 designed a superposition calculus for a clausal fragment of extensional
polymorphic higher-order logic that includes anonymous functions but excludes
Booleans. The inference rules work on $\beta\eta$-equivalence classes of
$\lambda$-terms and rely on higher-order unification to achieve refutational
completeness. We implemented the calculus in the Zipperposition prover and
evaluated it on TPTP and Isabelle benchmarks. The results suggest that
superposition is a suitable basis for higher-order reasoning.

Details

show
hide
Language(s): eng - English
 Dates: 2021-01-312021
 Publication Status: Published online
 Pages: 45 p.
 Publishing info: -
 Table of Contents: -
 Rev. Type: -
 Identifiers: arXiv: 2102.00453
URI: https://arxiv.org/abs/2102.00453
BibTex Citekey: Bentkamp2102.00453
 Degree: -

Event

show

Legal Case

show

Project information

show

Source

show