Goal-oriented conjecturing for Isabelle/HOL

DOI10.1007/978-3-319-96812-4_19MaRDI QIDQ1798971zbMATH OpenOpenAlexFDO

Authors Yutaka Nagashima, Julian Parsert

Publication date 18 October 2018

Full work available at URL https://arxiv.org/abs/1806.04774

Mathematics Subject Classification ID

Abstract: We present PGT, a Proof Goal Transformer for Isabelle/HOL. Given a proof goal and its background context, PGT attempts to generate conjectures from the original goal by transforming the original proof goal. These conjectures should be weak enough to be provable by automation but sufficiently strong to prove the original goal. By incorporating PGT into the pre-existing PSL framework, we exploit Isabelle's strong automation to identify and prove such conjectures.

Recommendations

• A proof strategy language and proof script generation for Isabelle/HOL
• Semi-intelligible Isar proofs from machine-generated proofs
• Automatic proof and disproof in Isabelle/HOL
• Conjecture synthesis for inductive theories
• scientific article; zbMATH DE number 1552515

Cited in

(5)

• Conjecture synthesis for inductive theories
• Journal on Data Semantics I
• A goal-type driven method of solving Horn logic with equality
• Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
• A proof strategy language and proof script generation for Isabelle/HOL

Describes a project that uses

Uses Software

• HOL
• Isabelle/HOL
• Isabelle

This page was built for publication: Goal-oriented conjecturing for Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1798971)