Superposition for Lambda-Free Higher-Order Logic

Alexander Bentkamp; Jasmin Blanchette; Simon Cruanes; Uwe Waldmann

REVIEW

Superposition for Lambda-Free Higher-Order Logic

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2005.02094 v4 pith:SNADJSOI submitted 2020-05-05 cs.LO cs.AI

Superposition for Lambda-Free Higher-Order Logic

Alexander Bentkamp , Jasmin Blanchette , Simon Cruanes , Uwe Waldmann This is my paper

classification cs.LO cs.AI

keywords higher-ordercalculilogiccompletefreelambdasuperpositionallow

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

0 comments

read the original 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.

Superposition for Lambda-Free Higher-Order Logic

discussion (0)