Name
Abstract | ||
|---|---|---|
Well-known principles of induction include monotone induction and different sorts of nonmonotone induction such as inflationary induction, induction over well-founded sets and iterated induction. In this work, we define a logic formalizing induction over well-founded sets and monotone and iterated induction. Just as the principle of positive induction has been formalized in FO(LFP), and the principle of inflationary induction has been formalized in FO(IFP), this article formalizes the principle of iterated induction in a new logic for Nonmonotone Inductive Definitions (ID-logic). The semantics of the logic is strongly influenced by the well-founded semantics of logic programming. This article discusses the formalisation of different forms of (non-)monotone induction by the well-founded semantics and illustrates the use of the logic for formalizing mathematical and common-sense knowledge. To model different types of induction found in mathematics, we define several subclasses of definitions, and show that they are correctly formalized by the well-founded semantics. We also present translations into classical first or second order logic. We develop modularity and totality results and demonstrate their use to analyze and simplify complex definitions. We illustrate the use of the logic for temporal reasoning. The logic formally extends Logic Programming, Abductive Logic Programming and Datalog, and thus formalizes the view on these formalisms as logics of (generalized) inductive definitions. |
Year | DOI | Venue |
|---|---|---|
2008 | 10.1145/1342991.1342998 | ACM Trans. Comput. Log. |
Keywords | Field | DocType |
classical logic,nonmonotone inductive definition,monotone induction,new logic,well-founded semantics,logic programming,well-founded set,well-known principle,inductive definitions,order logic,positive induction,iterated induction,inflationary induction,languages,abductive logic programming,fixpoint,theory,second order | Discrete mathematics,Computational logic,Multimodal logic,Many-valued logic,Predicate logic,Dynamic logic (modal logic),Mathematics,Intermediate logic,Structural induction,Higher-order logic | Journal |
Volume | Issue | ISSN |
9 | 2 | 1529-3785 |
Citations | PageRank | References |
35 | 1.28 | 33 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Marc Denecker | 1 | 1626 | 106.40 |
| Eugenia Ternovska | 2 | 211 | 15.05 |