Clasificación por Disciplina
Nomenclatura Unesco > (11) Lógica > (1104) Lógica inductiva
- (1104.01) Inducción
- (1104.02) Intuicionismo
- (1104.03) Probabilidad
- (1104.99) Otras (especificar)
Nomenclatura Unesco > (11) Lógica > (1104) Lógica inductiva
Chen, Ran; Levy, Jean-Jacques
Quite often formal proofs are not published in conferences or journal articles, because formal proofs are usually too long. A typical article states the ability of having implemented a formal proof, but the proof itself is often sketched in terms of a natural language. At best, some formal lemmas and definitions are stated. Can we do better ? We try here to publish the details of a formal proof of the white-paths theorem about depth-first search in graphs. We use Why3 as the proving platform, because Why3 uses first-order logic augmented with inductive definitions of predicates and because Why3 makes...
Jaume, Mathieu
International audience
Ribeiro, Tony; Tourret, Sophie; Folschette, Maxime; Magnin, Morgan; Borzacchiello, Domenico; Chinesta, Francisco; Roux, Olivier; Inoue, Katsumi
Presented at: 27th International Conference on Inductive Logic Programming (ILP 2017). To be published in Lecture Notes in Artificial Intelligence.
Ribeiro, Tony; Tourret, Sophie; Folschette, Maxime; Magnin, Morgan; Borzacchiello, Domenico; Chinesta, Francisco; Roux, Olivier; Inoue, Katsumi
Presented at: 27th International Conference on Inductive Logic Programming (ILP 2017). To be published in Lecture Notes in Artificial Intelligence.
Ribeiro, Tony; Tourret, Sophie; Folschette, Maxime; Magnin, Morgan; Borzacchiello, Domenico; Chinesta, Francisco; Roux, Olivier; Inoue, Katsumi
Presented at: 27th International Conference on Inductive Logic Programming (ILP 2017). To be published in Lecture Notes in Artificial Intelligence.
Ribeiro, Tony; Tourret, Sophie; Folschette, Maxime; Magnin, Morgan; Borzacchiello, Domenico; Chinesta, Francisco; Roux, Olivier; Inoue, Katsumi
Presented at: 27th International Conference on Inductive Logic Programming (ILP 2017). To be published in Lecture Notes in Artificial Intelligence.
Carrault, Guy; Cordier, Marie-Odile; Quiniou, René; Wang, F.
International audience
Carrault, Guy; Cordier, Marie-Odile; Quiniou, René; Wang, F.
International audience
Ozdowska, Sylwia; Claveau, Vincent
International audience
Ozdowska, Sylwia; Claveau, Vincent
International audience
Ozdowska, Sylwia; Claveau, Vincent
International audience
Davis, Jesse; Ramon, Jan
International audience
Davis, Jesse; Ramon, Jan
International audience
Silva Bernardes, Juliana
International audience
Minato, Shin-ichi
Discrete structures are foundational material for computer science and mathematics, which are related to set theory, symbolic logic, inductive proof, graph theory, combinatorics, probability theory, etc. Many problems solved by computers can be decomposed into discrete structures using simple primitive algebraic operations. It is very important to represent discrete structures compactly and to execute efficiently tasks such as equivalency/validity checking, analysis of models, and optimization. Recently, BDDs (Binary Decision Diagrams) and ZDDs (Zero-suppressed BDDs) have attracted a great deal of attention, because they efficiently represent and manipulate large-scale combinational logic data, which are the basic discrete structures in various fields...
Read, Carveth,
1848-1931
Mode of access: Internet.
Rowe, RNS; Brotherston, J
© 2017 ACM.We describe a formal verification framework and tool implementation, based upon cyclic proofs, for certifying the safe termination of imperative pointer programs with recursive procedures. Our assertions are symbolic heaps in separation logic with user defined inductive predicates; we employ explicit approximations of these predicates as our termination measures. This enables us to extend cyclic proof to programs with procedures by relating these measures across the preand postconditions of procedure calls. We provide an implementation of our formal proof system in the CYCLIST theorem proving framework, and evaluate its performance on a range of examples drawn from the...
Rusu, Vlad; Clavel, Manuel
We present an approach based on inductive theorem proving for verifying invariance properties of systems specified in Rewriting Logic, an executable specification language implemented (among others) in the Maude tool. Since theorem proving is not directly available for rewriting logic, we define an encoding of rewriting logic into its membership equational (sub)logic. Then, inductive theorem provers for membership equational logic, such as the itp tool, can be used for verifying the resulting membership equational logic specification, and, implicitly, for verifying invariance properties of the original rewriting logic specification. The approach is illustrated first on a 2-process Bakery algorithm and then...
Lin, Dianhuan; Dechter, Eyal; Ellis, Kevin M.; Tenenbaum, Joshua B.; Muggleton, Stephen H.
In recent years predicate invention has been underexplored as a bias reformulation mechanism within Inductive Logic Programming due to difficulties in formulating efficient search mechanisms. However, recent papers on a new approach called Meta-Interpretive Learning have demonstrated that both predicate invention and learning recursive predicates can be efficiently implemented for various fragments of definite clause logic using a form of abduction within a meta-interpreter. This paper explores the effect of bias reformulation produced by Meta-Interpretive Learning on a series of Program Induction tasks involving string transformations. These tasks have real-world applications in the use of spreadsheet technology. The existing implementation...
Dubba, KSR; Cohn, AG; Hogg, DC
Learning event models from videos has applications ranging from abnormal event detection to content based video retrieval. Relational learning techniques such as Inductive Logic Programming (ILP) hold promise for building such models, but have not been successfully applied to the very large datasets which result from video data. In this paper we present a novel supervised learning framework to learn event models from large video datasets (~2.5 million frames) using ILP. Efficiency is achieved via the learning from interpretations setting and using a typing system. This allows learning to take place in a reasonable time frame with reduced false positives....