Sun, 27 Jul 2008 08:15:13 BST CiteULike: gabgas's library [26 articles] http://www.citeulike.org/user/gabgas/order/to_read CiteULike.org en-gb Copyright © 2004-2008 citeulike.org http://www.citeulike.org/user/gabgas/article/259185 <i>Pattern Recognition, Vol. 38, No. 9. (September 2005), pp. 1349-1371.</i><br /><br />This article presents an overview of Probabilistic Automata (PA) and discrete Hidden Markov Models (HMMs), and aims at clarifying the links between them. The first part of this work concentrates on probability distributions generated by these models. Necessary and sufficient conditions for an automaton to define a probabilistic language are detailed. It is proved that probabilistic deterministic automata (PDFA) form a proper subclass of probabilistic non-deterministic automata (PNFA). Two families of equivalent models are described next. On one hand, HMMs and PNFA with no final probabilities generate distributions over complete finite prefix-free sets. On the other hand, HMMs with final probabilities and probabilistic automata generate distributions over strings of finite length. The second part of this article presents several learning models, which formalize the problem of PA induction or, equivalently, the problem of HMM topology induction and parameter estimation. These learning models include the PAC and identification with probability 1 frameworks. Links with Bayesian learning are also discussed. The last part of this article presents an overview of induction algorithms for PA or HMMs using state merging, state splitting, parameter pruning and error-correcting techniques. Links between probabilistic automata and hidden Markov models: probability distributions, learning models and induction algorithms P Dupont F Denis Y Esposito doi:10.1016/j.patcog.2004.03.020 Pattern Recognition, Vol. 38, No. 9. (September 2005), pp. 1349-1371. 2005-07-19T08:07:50-00:00 2005 Pattern Recognition 38 9 1349 1371 automata probabilistic http://www.citeulike.org/user/gabgas/article/849490 <i>Journal of Automated Reasoning, Vol. 26, No. 2. (2001), pp. 161-203.</i><br /><br />Experience has shown that large or multi-user interactive proof efforts can benefit significantly from structuring mechanisms, much like those available in many modern programming languages. Such a mechanism can allow some lemmas and definitions to be exported, and others not. In this paper we address two such structuring mechanisms for the ACL2 theorem prover: encapsulation and books. After presenting an introduction to ACL2, this paper justifies the implementation of ACL2's structuring... Structured Theory Development for a Mechanized Logic Matt Kaufmann Strother Moore Journal of Automated Reasoning, Vol. 26, No. 2. (2001), pp. 161-203. 2006-09-19T07:21:01-00:00 2001 Journal of Automated Reasoning 26 2 161 203 acl2 proving theorem http://www.citeulike.org/user/gabgas/article/2138375 <i>Automated Deduction – CADE-19 (2003), pp. 279-283.</i><br /><br />IsaPlanner is a generic framework for proof planning in the interactive theorem prover Isabelle. It facilitates the encoding of reasoning techniques, which can be used to conjecture and prove theorems automatically. This paper introduces our approach to proof planning, gives and overview of IsaPlanner, and presents one simple yet effective reasoning technique. IsaPlanner: A Prototype Proof Planner in Isabelle Lucas Dixon Jacques Fleuriot Automated Deduction – CADE-19 (2003), pp. 279-283. 2007-12-17T21:43:14-00:00 2003 Automated Deduction – CADE-19 279 283 planning proof http://www.citeulike.org/user/gabgas/article/1885958 <i></i><br /><br />It is critical to have an induction method for reasoning about recursive programs expressed as fixed points, for otherwise our reasoning ability is severely impaired. The fixed point induction rule developed by deBakker and Scott is one such well known principle. Here we propose a new induction method, computational induction, which is an induction on the computation process. Computational induction is founded on different principles than the fixed point induction principle---it can only be... A Computational Induction Principle Scott Smith 2007-11-08T19:51:57-00:00 proving theorem http://www.citeulike.org/user/gabgas/article/1271098 <i>(2001)</i><br /><br />this paper, we will flesh out this remark by discussing the following topics: An introduction to graphical models K Murphy (2001) 2007-05-02T07:32:01-00:00 2001 learning machine http://www.citeulike.org/user/gabgas/article/2582936 <i>(2006), pp. 65-74.</i> Comparing XML path expressions Pierre Genevès Nabil Laya\ida doi:10.1145/1166160.1166182 (2006), pp. 65-74. 2008-03-24T22:39:59-00:00 2006 65 74 ACM document engineering http://www.citeulike.org/user/gabgas/article/2178367 <i>Journal of Mathematical Psychology, Vol. 51, No. 3. (June 2007), pp. 135-163.</i><br /><br />Gold's [1967. Language identification in the limit. Information and Control, 16, 447-474] celebrated work on learning in the limit has been taken, by many cognitive scientists, to have powerful negative implications for the learnability of language from positive data (i.e., from mere exposure to linguistic input). This provides one, of several, lines of argument that language acquisition must draw on other sources of information, including innate constraints on learning. We consider an `ideal learner' that applies a Simplicity Principle to the problem of language acquisition. The Simplicity Principle chooses the hypothesis that provides the briefest representation of the available data--here, the data are the linguistic input to the child. The Simplicity Principle allows learning from positive evidence alone, given quite weak assumptions, in apparent contrast to results on language learnability in the limit (e.g., Gold, 1967). These results provide a framework for reconsidering the learnability of various aspects of natural language from positive evidence, which has been at the center of theoretical debate in research on language acquisition and linguistics. `Ideal learning' of natural language: Positive results about learning from positive evidence Nick Chater Paul Vitanyi doi:10.1016/j.jmp.2006.10.002 Journal of Mathematical Psychology, Vol. 51, No. 3. (June 2007), pp. 135-163. 2007-12-29T01:25:29-00:00 2007 Journal of Mathematical Psychology 51 3 135 163 language learning natural unsupervised http://www.citeulike.org/user/gabgas/article/2194597 <i>ACM Computing Surveys, Vol. 33, No. 1. (2001), pp. 1-30.</i><br /><br />Many tasks require "reasoning" --- i.e., deriving conclusions from a corpus of explicitly stored information --- to solve their range of problems. An ideal reasoning system would produce alland -only the correct answers to every possible query, produce answers that are as specific as possible, be expressive enough to permit any possible fact to be stored and any possible query to be asked, and be efficient. Unfortunately, this is provably impossible: as correct and precise systems become more... Efficient reasoning Russell Greiner Christian Darken Iwan Santoso ACM Computing Surveys, Vol. 33, No. 1. (2001), pp. 1-30. 2008-01-04T13:50:05-00:00 2001 ACM Computing Surveys 33 1 1 30 learning logic machine probabilistic http://www.citeulike.org/user/gabgas/article/2189886 <i>Minds and Machines, Vol. 7, No. 3. (1997), pp. 409-424.</i><br /><br />Without Abstract Goals for a Theory of Deduction: Reply to Johnson-Laird Lance Rips doi:10.1023/A:1008234725870 Minds and Machines, Vol. 7, No. 3. (1997), pp. 409-424. 2008-01-02T21:15:28-00:00 1997 Minds and Machines 7 3 409 424 proof psychology http://www.citeulike.org/user/gabgas/article/2189289 <i>Transactions on Computers, Vol. C-25, No. 4. (1976), pp. 328-334.</i><br /><br />A semantic and deductive formal system for automatic theorem proving is presented. The system has, as its deductive component, a form of natural deduction. Its semantic component relies on an underlying representation of a model. This model is invoked to prune subgoals generated by the deductive component, whenever such subgoals test false in the model. In addition, the model is used to suggest inferences to be made at the deductive level. Conversely, the current state of the proof suggests changes to be made to the model, e.g., when a construction is required as in geometry. A Semantically Guided Deductive System for Automatic Theorem Proving R Reiter doi:10.1109/TC.1976.1674613 Transactions on Computers, Vol. C-25, No. 4. (1976), pp. 328-334. 2008-01-02T18:52:10-00:00 1976 Transactions on Computers C-25 4 328 334 planning proof http://www.citeulike.org/user/gabgas/article/2152860 <i>Logic Jnl IGPL, Vol. 11, No. 6. (1 November 2003), pp. 647-673.</i><br /><br />In this paper we present an approach to automated learning within mathematical reasoning systems. In particular, the approach enables proof planning systems to automatically learn new proof methods from well-chosen examples of proofs which use a similar reasoning pattern to prove related theorems. Our approach consists of an abstract representation for methods and a machine learning technique which can learn methods using this representation formalism. We present an implementation of the approach within the OmegaMEGA proof planning system, which we call LEARNOmegaMATIC. We also present the results of the experiments that we ran on this implementation in order to evaluate if and how it improves the power of proof planning systems. 10.1093/jigpal/11.6.647 Automatic Learning of Proof Methods in Proof Planning Mateja Jamnik Manfred Kerber Martin Pollet Christoph Benzmuller doi:10.1093/jigpal/11.6.647 Logic Jnl IGPL, Vol. 11, No. 6. (1 November 2003), pp. 647-673. 2007-12-20T19:48:46-00:00 2003 Logic Jnl IGPL 11 6 647 673 planning proof http://www.citeulike.org/user/gabgas/article/1541917 <i>Artificial Intelligence, Vol. 64, No. 1. (1993), pp. 81-129.</i><br /><br />This paper presents a simple framework for Horn-clause abduction, with probabilities associated with hypotheses. The framework incorporates assumptions about the rule base and independence assumptions amongst hypotheses. It is shown how any probabilistic knowledge representable in a discrete Bayesian belief network can be represented in this framework. The main contribution is in finding a relationship between logical and probabilistic notions of evidential reasoning. This provides a useful... Probabilistic Horn Abduction and Bayesian Networks David Poole Artificial Intelligence, Vol. 64, No. 1. (1993), pp. 81-129. 2007-08-07T19:53:22-00:00 1993 Artificial Intelligence 64 1 81 129 inference logic probabilistic http://www.citeulike.org/user/gabgas/article/1438465 <i></i><br /><br />The application of automatic transformation processes during the formal development and optimization of programs can introduce encumbrances in the generated code that programmers usually (or presumably) do not write. An example is the introduction of redundant arguments in the functions defined in the program. Redundancy of a parameter means that replacing it by any expression does not change the result. In this work, we provide a method for the analysis and elimination of redundant... Removing Redundant Arguments Automatically M Alpuente S Escobar S Lucas 2007-07-05T23:59:27-00:00 no-tag http://www.citeulike.org/user/gabgas/article/1439479 <i></i><br /><br />As machine-oriented approaches to automated theorem proving are apparently revealing limitations, human-oriented approaches offer the chance to overcome some of these limitations for many problem domains. Proof planning is the best studied approach to human-oriented theorem proving. As in any search procedure, the key problem is that we do not have a satisfyingly reliable strategy as to what method to choose. Previous work on proof planning has left an important problem as to which method to... Semantically Guided Proof Planning Seungyeob Choi 2007-07-06T12:49:58-00:00 planning proof