Induction with Generalization in Superposition Reasoning

被引：12

作者：

Hajdu, Marton ^{[1
]}

Hozzova, Petra ^{[1
]}

Kovacs, Laura ^{[1
,2
]}

Schoisswohl, Johannes ^{[1
,3
]}

Voronkov, Andrei ^{[3
,4
]}

机构：

[1] TU Wien, Vienna, Austria

[2] Chalmers Univ Technol, Gothenburg, Sweden

[3] Univ Manchester, Manchester, England

[4] EasyChair, Manchester, England

来源：

INTELLIGENT COMPUTER MATHEMATICS, CICM 2020 | 2020年 / 12236卷

基金：

英国工程与自然科学研究理事会;

关键词：

D O I：

10.1007/978-3-030-53518-6_8

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We describe an extension of automating induction in superposition-based reasoning by strengthening inductive properties and generalizing terms over which induction should be applied. We implemented our approach in the first-order theorem prover Vampire and evaluated our work against state-of-the-art reasoners automating induction. We demonstrate the strength of our technique by showing that many interesting mathematical properties of natural numbers and lists can be proved automatically using this extension.

引用

页码：123 / 137

页数：15

共 50 条

[1] A Superposition Calculus for Abductive Reasoning
Echenim, M.
Peltier, N.
[J]. JOURNAL OF AUTOMATED REASONING, 2016, 57 (02) : 97 - 134
[2] A Superposition Calculus for Abductive Reasoning
M. Echenim
N. Peltier
[J]. Journal of Automated Reasoning, 2016, 57 : 97 - 134
[3] Analogical reasoning and generalization
不详
[J]. INDUCTIVE SYNTHESIS OF FUNCTIONAL PROGRAMS: UNIVERSAL PLANNING, FOLDING OF FINITE PROGRAMS, AND SCHEMA ABSTRACTION BY ANALOGICAL REASONING, 2003, 2654 : 279 - 290
[4] Symbolic Representation and Reasoning for Rectangles with Superposition
Konishi, Takako
Takahashi, Kazuko
[J]. DBKDA 2011: THE THIRD INTERNATIONAL CONFERENCE ON ADVANCES IN DATABASES, KNOWLEDGE, AND DATA APPLICATIONS, 2011, : 71 - 76
[5] Superposition with Structural Induction
Cruanes, Simon
[J]. FRONTIERS OF COMBINING SYSTEMS (FROCOS 2017), 2017, 10483 : 172 - 188
[6] Trends of progression of student level of reasoning and generalization in numerical and figural reasoning approaches in pattern generalization
El Mouhayar, Rabih
[J]. EDUCATIONAL STUDIES IN MATHEMATICS, 2018, 99 (01) : 89 - 107
[7] Trends of progression of student level of reasoning and generalization in numerical and figural reasoning approaches in pattern generalization
Rabih El Mouhayar
[J]. Educational Studies in Mathematics, 2018, 99 : 89 - 107
[8] Similarity, induction, naming, and categorization (SINC): Generalization or inductive reasoning? Reply to Heit and Hayes (2005)
Sloutsky, VM
Fisher, AV
[J]. JOURNAL OF EXPERIMENTAL PSYCHOLOGY-GENERAL, 2005, 134 (04) : 606 - 611
[9] A Superposition-Based Calculus for Diagrammatic Reasoning
Echahed, Rachid
Echenim, Mnacho
Mhalla, Mehdi
Peltier, Nicolas
[J]. PROCEEDINGS OF THE 23RD INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, PPDP 2021, 2021,
[10] Superposition Reasoning about Quantified Bitvector Formulas
Damestani, David
Kovacs, Laura
Suda, Martin
[J]. 2019 21ST INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC 2019), 2020, : 95 - 99

← 1 2 3 4 5 →