Superposition with Lambdas

被引：17

作者：

Bentkamp, Alexander ^{[1
]}

Blanchette, Jasmin ^{[1
,2
]}

Tourret, Sophie ^{[2
]}

Vukmirovic, Petar ^{[1
]}

Waldmann, Uwe ^{[2
]}

机构：

[1] Vrije Univ Amsterdam, Amsterdam, Netherlands

[2] Max Planck Inst Informat, Saarland Informat Campus, Saarbrucken, Germany

来源：

AUTOMATED DEDUCTION, CADE 27 | 2019年 / 11716卷

基金：

欧洲研究理事会;

关键词：

HIGHER-ORDER UNIFICATION; NORMAL-FORM;

D O I：

10.1007/978-3-030-29436-6_4

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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.-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.

引用

页码：55 / 73

页数：19

共 64 条

[1]

Andrews P. B., 1989, Journal of Automated Reasoning, V5, P257, DOI 10.1007/BF00248320

[2] RESOLUTION IN TYPE THEORY [J].

ANDREWS, PB .

JOURNAL OF SYMBOLIC LOGIC, 1971, 36 (03) :414-&

[3] TPS: A theorem-proving system for classical type theory [J].

Andrews, PB ;

Bishop, M ;

Issar, S ;

Nesmith, D ;

Pfenning, F ;

Xi, HW .

JOURNAL OF AUTOMATED REASONING, 1996, 16 (03) :321-353

[4]

[Anonymous], 2012, IWIL 2010 EPIC

[5]

[Anonymous], 2002, Types, Tableaus, and Godel's God

[6]

Bachmair L., 1994, Journal of Logic and Computation, V4, P217, DOI 10.1093/logcom/4.3.217

[7] Analytic Tableaux for Higher-Order Logic with Choice [J].

Backes, Julian ;

Brown, Chad Edward .

JOURNAL OF AUTOMATED REASONING, 2011, 47 (04) :451-479

[8]

Barbosa H., 2018, SMT 2018

[9] A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms [J].

Becker, Heiko ;

Blanchette, Jasmin Christian ;

Waldmann, Uwe ;

Wand, Daniel .

AUTOMATED DEDUCTION - CADE 26, 2017, 10395 :432-453

[10]

Bentkamp A., 2018, ARCH FORMAL PROOFS

← 1 2 3 4 5 6 7 →