Extracting Higher-Order Goals from the Mizar Mathematical Library

Chad Brown; Josef Urban

REVIEW

Extracting Higher-Order Goals from the Mizar Mathematical Library

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 1605.06996 v1 pith:SDYVIHJS submitted 2016-05-23 cs.LO cs.AI

Chad Brown , Josef Urban This is my paper

classification cs.LOcs.AI

keywords higher-orderlogicmizararticlesconstructsproblemsrepresentedtheorem

verification ladder T0 review T1 audit T2 compute T3 formal

0 comments

read the original abstract

Certain constructs allowed in Mizar articles cannot be represented in first-order logic but can be represented in higher-order logic. We describe a way to obtain higher-order theorem proving problems from Mizar articles that make use of these constructs. In particular, higher-order logic is used to represent schemes, a global choice construct and set level binders. The higher-order automated theorem provers Satallax and LEO-II have been run on collections of these problems and the results are discussed.

Discussion (0). Sign in to comment.

Pith tools