SOME OBSERVATIONS ON THE LOGICAL FOUNDATIONS OF INDUCTIVE THEOREM PROVING

被引：4

作者：

Hetzl, Stefan ^{[1
]}

Wong, Tin Lok ^{[2
]}

机构：

[1] Vienna Univ Technol, Inst Discrete Math & Geometry, Wiedner Hauptstr 8-10, AT-1040 Vienna, Austria

[2] Univ Vienna, Kurt Godel Res Ctr Math Log, Wahringer Str 25, AT-1090 Vienna, Austria

来源：

LOGICAL METHODS IN COMPUTER SCIENCE | 2017年 / 13卷 / 04期

基金：

奥地利科学基金会;

关键词：

inductive theorem proving; arithmetical theories; proof theory; CHECKING; MODEL;

D O I：

10.23638/LMCS-13(4:10)2017

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

In this paper we study the logical foundations of automated inductive theorem proving. To that aim we first develop a theoretical model that is centered around the difficulty of finding induction axioms which are sufficient for proving a goal. Based on this model, we then analyze the following aspects: the choice of a proof shape, the choice of an induction rule and the language of the induction formula. In particular, using model-theoretic techniques, we clarify the relationship between notions of inductiveness that have been considered in the literature on automated inductive theorem proving.

引用

页数：26

共 50 条

[31] FOR COMPLEAT LOGICAL EMPIRICIST - NON-COGNITIVE FOUNDATIONS FOR INDUCTIVE LOGIC
CREARY, LG
[J]. AMERICAN PHILOSOPHICAL QUARTERLY, 1973, 10 (02) : 123 - 131
[32] Conditional equational specifications of data types with partial operations for inductive theorem proving
Kuhler, U
Wirth, CP
[J]. REWRITING TECHNIQUES AND APPLICATIONS, 1997, 1232 : 38 - 52
[33] Inductive theorem proving by program specialisation: Generating proofs for Isabelle using ECCE
Lehmann, H
Leuschel, M
[J]. LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2003, 3018 : 1 - 19
[34] Revising the logical foundations of inductive logic programming systems with ground reduced programs
Yamamoto, A
[J]. NEW GENERATION COMPUTING, 1999, 17 (01) : 119 - 127
[35] Revising the logical foundations of inductive logic programming systems with ground reduced programs
Akihiro Yamamoto
[J]. New Generation Computing, 1999, 17 : 119 - 127
[36] Some Observations on the FGH Theorem
Kurahashi, Taishi
[J]. STUDIA LOGICA, 2023, 111 (05) : 749 - 778
[37] Some Observations on the FGH Theorem
Taishi Kurahashi
[J]. Studia Logica, 2023, 111 : 749 - 778
[38] THEOREM-PROVING FOR COMPUTERS - SOME RESULTS ON RESOLUTION AND RENAMING
MELTZER, B
[J]. COMPUTER JOURNAL, 1966, 8 (04): : 341 - &
[39] SOME REMARKS ON MECHANICAL THEOREM-PROVING IN ELEMENTARY GEOMETRY
吴文俊
[J]. Acta Mathematica Scientia, 1983, (04) : 357 - 360
[40] THE NATURE AND APPLICATION OF INDUCTIVE LOGIC: CONSISTING OF SIX SECTIONS FROM "LOGICAL FOUNDATIONS OF PROBABILITY"
Burks, Arthur W.
[J]. ETHICS, 1951, 62 (01) : 76 - 76

← 1 2 3 4 5 →