Publications
123 results found
Garcez ASD, Broda K, Gabbay DM, 2001, Symbolic knowledge extraction from trained neural networks: A sound approach, ARTIFICIAL INTELLIGENCE, Vol: 125, Pages: 155-207, ISSN: 0004-3702
- Author Web Link
- Cite
- Citations: 124
Broda KB, Hogger CJ, Watson S, 2000, Constructing Teleo-reactive Robot Programs, Proc. of the 14th European Conference on Artificial Intelligence (ECAI-2000), Publisher: IOS Press, Pages: 653-657
Broda KB, Gabbay DM, 2000, Labelled Abduction (I): Compiled Labelled Abductive Systems, Labelled Deduction, Editors: D'Agostino, Basin, Gabbay, Vigano, Publisher: Kluwer
Broda KB, Hogger CJ, Watson S, 2000, Constructing Teleo-reactive Programs, ECAI-2000 Berlin
Broda KB, Hogger CJ, Watson S, 2000, Constructing Teleo-reactive Programs, ECAI-2000 Berlin
Broda KB, Russo AM, Gabbay DM, 2000, A Unified Compilation Style Natural Deduction System for Modal, Substructural and Fuzzy Logics, Discovering World with Fuzzy Logic: Perspectives and Approaches to Formalization of Human-consistent Logical Systems, Editors: Novak, Perfileva, Novak, Perfileva, Publisher: Springer-Verlag
Russo A, Broda K, Finger M, 1999, Labelled Natural Deduction for Substructural Logics, Logic Journal of the IGPL, Vol: 7, Pages: 283-318, ISSN: 1367-0751
Broda KB, Finger M, Russo AM, 1999, LDS-Natural Deduction for Substructural Logics, IGPL, Vol: 7
Avila Garcez A, Broda KB, Gabbay DM, et al., 1999, Knowledge Extraction from Trained Neural Networks, IEEE International Conference on Neural Processing, ICONIP99, Perth, Australia
Broda KB, Gabbay DM, 1999, A Compiled Labelled Deductive System for Propositional Intuitionistic Logic, Proceedings of Tableaux 99, Saratoga Springs USA
Broda K, Gabbay D, 1999, CLDS for Propositional Intuitionistic Logic, Publisher: Springer Berlin Heidelberg, Pages: 66-82, ISSN: 0302-9743
D'Agostino M, Gabbay DM, Broda KB, 1999, Tableau Methods for Substructural Logics, Handbook of Tableaux Methods, Editors: D'Agostino, Gabbay, Hahnle, Possega, Publisher: Kluwer Academic Publishers
d'Avila Garcez AS, Broda K, Gabbay D, 1998, Symbolic knowledge extraction from trained neural networks: a new approach, Departmental Technical Report: 98/14/14a, Publisher: Department of Computing, Imperial College London
In this report, we investigate the problem of symbolic knowledge extraction from trained neural networks, and present a new extraction method. Although neural networks have shown very good performance in terms of learnability, generalizability and speed in many application domains, one of their main drawbacks lies in their incapacity to provide an explanation to the underlying reasoning mechanisms that justify a given answer. As a result, their use in many application areas, for instance in safety-critical domains, has become limited. The so called "explanation capability" of neural networks can be achieved by the extraction of symbolic knowledge from it, using "rules extraction" methods.We start by discussing some of the main problems of knowledge extraction methods. In an attempt to ameliorate these problems, we identify, in the case of neural networks, a partial ordering on the input vector space. A number of pruning rules and simplification rules that interact with this ordering are defined. These rules are used in our extraction algorithm in order to help reduce the input vector search space during a pedagogical knowledge extraction from trained networks. They are also very useful in helping to reduce the number of rules extracted, which provides clarity and readability to the rule set. We show that, in the case of regular networks, the extraction algorithm is sound and complete.We proceed to extend the extraction algorithm to the class of non-regular networks, the general case. We identify that non-regular networks contain regularities in their subnetworks. As a result, the underlying extraction method for regular networks can be applied, but now in decomposable fashion. The problem, however, is how to combine the set of rules extracted from each subnetwork into the final rule set. We propose a solution to this problem in which we are able to keep the soundness of the extraction algorithm, although we have to drop completeness.
Broda KB, 1998, Algorithms for Implication LKE, Presented at LDS98, Dept. Comp. Sci. Albert-Ludwigs University, Friburg, Germany
Broda KB, D'Agostino M, Russo AM, 1998, Transformation Methods in LDS, Logic, Language and Reasoning: An Essay in Honour of Gabbay, Editors: Ohlbach, Ohlbach, Publisher: Kluwer
Broda K, Finger M, Russo A, 1997, Labelled natural deduction for substructural logics, Departmental Technical Report: 97/11
In this paper a uniform methodology to perform Natural Deduction over the family of linear, relevance and intuitionistic logics is proposed. The methodology follows the Labelled Deductive Systems (LDS) discipline, where the deductive process manipulates declarative units - formulas labelled according to a labelling algebra. In the system described here, labels are either ground terms or variables of a given labelling language and inference rules manipulate formulas and labels simultaneously, generating (whenever necessary) constraints on the labels used in the rules. A set of natural deduction style inference rules is given, and the notion of a derivation is defined which associates a labelled natural deduction style "structural derivation" with a set of generated constraints. Algorithmic procedures, based on a technique called resource abduction, are defined to solve the constraints generated within a derivation, and their termination conditions discussed. A natural deduction derivation is correct with respect to a given substructural logic, if, under the condition that the algorithmic procedures terminate, the associated set of constraints is satisfied with respect to the underlying labelling algebra. This is shown by proving that the natural deduction system is sound and complete with respect to the LKE tableaux system.
Broda K, Russo A, 1997, A unified compilation style labelled deductive system for modal and substructural logic using natural deduction, Departmental Technical Report: 97/10, Publisher: Department of Computing, Imperial College London
This paper describes a proof theoretic and semantic approach in which logics belonging to different families can be given common notions of derivability relation and semantic entailment. This approach builds upon Gabbay's methodology of Labelled Deductive Systems (LDS) and it is called the compilation approach for labelled deductive systems (CLDS). Two different logics are here considered, (i) the modal logic of elsewhere (known also as the logic of inequality) and (ii) the multiplicative fragment of substructural linear logic. A general natural deduction style proof system is given, in which the notion of a theory is defined as a (possibly singleton) structure of points, called a configuration, and a "general" model-theoretic semantic approach is described using a translation technique based on first-order logic. Then it is shown how both this proof theory and semantics can be directly applied to the logic of elsewhere and to linear logic, illustrating also that the same technique for proving soundness and completeness can be adopted in both logics. Finally, the proof systems for the logic of elsewhere and for linear logic are proved to correspond, under certain conditions, to standard Hilbert axiomatisation and standard sequent calculus respectively. Such results prove that the natural deduction proof systems described in this paper are proper generalisations of any proof system already developed for these two logics.
Broda KB, Russo AM, 1997, Theorem Proving in LDS - A Compilation Approach, Proceedings of Workshop on Automated Reasoning, Manchester
Broda KB, D'Agostino M, Mondadori M, 1997, A Solution to a Problem of Popper, The Epistemology of Karl Popper, Publisher: Kluwer
Broda K, Russo A, 1997, A Unified Compilation Style Labelled Deductive System for Modal and Substructural Logic using Natural Deduction, Technical Report, Publisher: Imperial College London, Department of Computing
Broda KB, Mole D, 1996, Fault finding in a commercial requirements document as a student project for Z specification, Fourth annual CTI Conference on the teaching of Computing, Dublin
Broda KB, Finger M, Russo AM, 1996, LDS-Natural Deduction for Substructural Logics, WOLLIC 96
Broda KB, Eisenbach S, 1996, Tool Support for Informal Deduction, ACSE'96, Sydney, Australia
Broda KB, Eisenbach S, Kamara L, 1996, Tool Support for Natural Deduction, Proceedings of ACSE96, CACM
Broda KB, Eisenbach S, Kamara L, 1996, Tool Support for Natural Deduction, Proceedings of ACSE96, CACM
Broda KB, Finger M, 1995, KE Tableaux for a Fragment of Linear Logic, 4th International Workshop on Analytic Tableaux and Related Methods, St. Goar, Germany
Broda KB, D'Agostino M, Mondadori M, 1994, A Solution to a Problem of Popper, Conference presentation at Conference on the Epistemology of Karl Popper, Cesena
Broda KB, Eisenbach S, 1994, Teaching Program Reasoning in the First Year, NSF Teaching Formal Methods Workshop, New York
Broda KB, D'Agostino M, 1994, Finding Proofs in Substructural Logics, Conference presentation at Workshop in Proof Theory, Linear Logic and Categorical Grammars,Rome
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.