# A focused sequent calculus for higher-order logic

**Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)** (2014)

[Konferensbidrag, refereegranskat]

We present a focused intuitionistic sequent calculus for higher-order logic. It has primitive support for equality and mixes λ-term conversion with equality reasoning. Classical reasoning is enabled by extending the system with rules for reductio ad absurdum and the axiom of choice. The resulting system is proved sound with respect to Church's simple type theory. The soundness proof has been formalized in Agda. A theorem prover based on bottom-up search in the calculus has been implemented. It has been tested on the TPTP higher-order problem set with good results. The problems for which the theorem prover performs best require higher-order unification more frequently than the average higher-order TPTP problem. Being strong at higher-order unification, the system may serve as a complement to other theorem provers in the field.

(öppna i nytt fönster)

**Det verkar som att din webbläsare saknar möjlighet att visa PDF. Klicka Öppna i nytt fönster för att läsa.**

### Länka till denna publikation

### Dela på webben

### Skapa referens, olika format (klipp och klistra)

**Harvard**

Lindblad, F. (2014) *A focused sequent calculus for higher-order logic*.

** BibTeX **

@conference{

Lindblad2014,

author={Lindblad, Fredrik},

title={A focused sequent calculus for higher-order logic},

booktitle={Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},

isbn={9783319085869},

abstract={We present a focused intuitionistic sequent calculus for higher-order logic. It has primitive support for equality and mixes λ-term conversion with equality reasoning. Classical reasoning is enabled by extending the system with rules for reductio ad absurdum and the axiom of choice. The resulting system is proved sound with respect to Church's simple type theory. The soundness proof has been formalized in Agda. A theorem prover based on bottom-up search in the calculus has been implemented. It has been tested on the TPTP higher-order problem set with good results. The problems for which the theorem prover performs best require higher-order unification more frequently than the average higher-order TPTP problem. Being strong at higher-order unification, the system may serve as a complement to other theorem provers in the field.},

year={2014},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 236376

A1 Lindblad, Fredrik

T1 A focused sequent calculus for higher-order logic

YR 2014

T2 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SN 9783319085869

AB We present a focused intuitionistic sequent calculus for higher-order logic. It has primitive support for equality and mixes λ-term conversion with equality reasoning. Classical reasoning is enabled by extending the system with rules for reductio ad absurdum and the axiom of choice. The resulting system is proved sound with respect to Church's simple type theory. The soundness proof has been formalized in Agda. A theorem prover based on bottom-up search in the calculus has been implemented. It has been tested on the TPTP higher-order problem set with good results. The problems for which the theorem prover performs best require higher-order unification more frequently than the average higher-order TPTP problem. Being strong at higher-order unification, the system may serve as a complement to other theorem provers in the field.

LA eng

DO 10.1007/978-3-319-08587-6_5

LK http://dx.doi.org/10.1007/978-3-319-08587-6_5

OL 30

Denna post skapades 2016-05-12.

CPL Pubid: 236376