检索结果-内蒙古大学图书馆

6th international Workshop on the Implementation of logics, IWIL 2006 - Held at the 13th international conference on logic for programming, Artificial Intelligence and Reasoning

作者： Korovin, Konstantin University of Manchester United Kingdom

来源：评论

学校读者我要写书评

暂无评论

Hypothesis finding with proof theoretical appropriateness criteria

引用

thEORETICAL COMPUTER SCIENCE 2006年第1期350卷 140-162页

作者： Fronhöfer, B Yamamoto, A Kyoto Univ Grad Sch Informat Kyoto 6068501 Japan Tech Univ Dresden Dept Comp Sci D-01062 Dresden Germany

For two given formulae B and C with B does not satisfy C, hypothesis finding means to produce a formula S such that B boolean AND S satisfies C. Hypothesis finding, or variants thereof, is central to various types of inference, e.g., abductive inference, inductive inference, machine learning, and machine discovery. Clarifying the nature of hypothesis finding is still in its infancy, a situation similar to the establishment of logical foundations of inference related to induction and discovery. Although trivial solutions to hypothesis finding are easy to give, finding appropriate hypotheses still remains as a great challenge. A central role in this context plays the question, what it means for a hypothesis to be appropriate? In this paper we propose an answer to this question, which is based on proof theoretical criteria. this is in contrast to most previous approaches where appropriateness of hypotheses was based on concepts of semantical weakness in classical logic. More precisely, we use provability in Relevance logic instead of classical semantical entailment, we demand utmost exploitation of the inferential potential (deductive content) inherent in B -> C and we demand S to be a minimal deductive supplement to B -> C. Along these lines we developed the concept of a minimized residue hypothesis which also constitutes an interesting trade-off between 'logical smallness' and 'syntactical smallness'. Published by Elsevier B.V.

关键词： hypothesis finding connection method relevance logic residue hypotheses inductive logic abduction and knowledge discovery

来源：评论

学校读者我要写书评

暂无评论

Randomised restarted search in ILP

引用

MACHINE LEARNING 2006年第1-3期64卷 183-208页

作者： Zelezny, Filip Srinivasan, Ashwin Page, C. David, Jr. Czech Tech Univ CR-16635 Prague Czech Republic IBM India Res Lab New Delhi India Univ Wisconsin Madison WI USA

Recent statistical performance studies of search algorithms in difficult combinatorial problems have demonstrated the benefits of randomising and restarting the search procedure. Specifically, it has been found that if the search cost distribution of the non-restarted randomised search exhibits a slower-than-exponential decay (that is, a "heavy tail"), restarts can reduce the search cost expectation. We report on an empirical study of randomised restarted search in ILP. Our experiments conducted on a high-performance distributed computing platform provide an extensive statistical performance sample of five search algorithms operating on two principally different classes of ILP problems, one represented by an artificially generated graph problem and the other by three traditional classification benchmarks (mutagenicity, carcinogenicity, finite element mesh design). the sample allows us to (1) estimate the conditional expected value of the search cost (measured by the total number of clauses explored) given the minimum clause score required and a "cutoff" value (the number of clauses examined before the search is restarted), (2) estimate the conditional expected clause score given the cutoff value and the invested search cost, and (3) compare the performance of randomised restarted search strategies to a deterministic non-restarted search. Our findings indicate striking similarities across the five search algorithms and the four domains, in terms of the basic trends of both the statistics (1) and (2). Also, we observe that the cutoff value is critical for the performance of the search algorithm, and using its optimal value in a randomised restarted search may decrease the mean search cost (by several orders of magnitude) or increase the mean achieved score significantly with respect to that obtained with a deterministic non-restarted search.

关键词： inductive logic programming randomized search Monte Carlo study

来源：评论

学校读者我要写书评

暂无评论

Quantitative pharmacophore models with inductive logic programming

Quantitative pharmacophore models with inductive logic progr...

引用

13th international conference on inductive logic programming

作者： Srinivasan, Ashwin Page, David Camacho, Rui King, Ross Indian Inst Technol IBM India Res Lab New Delhi India Univ Madison Dept Biostat Madison WI USA LIACC CIUP P-4150 Oporto Portugal Univ Wales Dept Comp Sci Aberystwyth Dyfed Wales

three-dimensional models, or pharmacophores, describing Euclidean constraints on the location on small molecules of functional groups (like hydrophobic groups, hydrogen acceptors and donors, etc.), are often used in drug design to describe the medicinal activity of potential drugs (or 'ligands'). this medicinal activity is produced by interaction of the functional groups on the ligand with a binding site on a target protein. In identifying structure-activity relations of this kind there are three principal issues: (1) It is often difficult to "align" the ligands in order to identify common structural properties that may be responsible for activity;(2) Ligands in solution can adopt different shapes (or 'conformations') arising from torsional rotations about bonds. the 3-D molecular substructure is typically sought on one or more low-energy conformers;and (3) Pharmacophore models must, ideally, predict medicinal activity on some quantitative scale. It has been shown that the logical representation adopted by inductive logic programming (ILP) naturally resolves many of the difficulties associated with the alignment and multi-conformation issues. However, the predictions of models constructed by ILP have hitherto only been nominal, predicting medicinal activity to be present or absent. In this paper, we investigate the construction of two kinds of quantitative pharmacophoric models with ILP: (a) Models that predict the probability that a ligand is "active";and (b) Models that predict the actual medicinal activity of a ligand. Quantitative predictions are obtained by the utilising the following statistical procedures as background knowledge: logistic regression and naive Bayes, for probability prediction;linear and kernel regression, for activity prediction. the multi-conformation issue and, more generally, the relational representation used by ILP results in some special difficulties in the use of any statistical procedure. We present the principal issues and some solut

关键词： pharmacophore models ILP statistical relational learning

来源：评论

学校读者我要写书评

暂无评论

Representing defaults and negative information without negation-as-failure

引用

13th international conference on logic for programming, Artificial Intelligence, and Reasoning

作者： Fillottrani, Pablo R. Simari, Guillermo R. Univ Nacl Sur Dept Comp Sci & Engn Av Alem 1253 RA-8000 Bahia Blanca Buenos Aires Argentina

ISBN: (纸本)3540482814

In logic programs, negation-as-failure has been used both for representing negative information and for providing default non-monotonic inference. In this paper we argue that this twofold role is not only unnecessary for the expressiveness of the language, but it also plays against declarative programming, especially if further negation symbols such as strong negation are also available. We therefore propose a new logic programming approach in which negation and default inference are independent, orthogonal concepts. Semantical characterization of this approach is given in the style of answer sets, but other approaches are also possible. Finally, we compare them with the semantics for logic programs with two kinds of negation.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Modular cut-elimination: Finding proofs or counterexamples

引用

13th international conference on logic for programming, Artificial Intelligence, and Reasoning

作者： Ciabattoni, Agata Terui, Kazushige TU Vienna Inst Diskrete Math & Geometrie Vienna Austria Natl Inst Informat Tokyo Japan

ISBN: (纸本)3540482814

Modular cut-elimination is a particular notion of "cut-elimination in the presence of non-logical axioms" that is preserved under the addition of suitable rules. We introduce syntactic necessary and sufficient conditions for modular cut-elimination for standard calculi, a wide class of (possibly) multiple-conclusion sequent calculi with generalized quantifiers. We provide a "universal" modular cut-elimination procedure that works uniformly for any standard calculus satisfying our conditions. the failure of these conditions generates counterexamples for modular cut-elimination and, in certain cases, for cut-elimination.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

theory instantiation

引用

13th international conference on logic for programming, Artificial Intelligence, and Reasoning

作者： Ganzinger, Harald Korovin, Konstantin MPI Informat Saarbrucken Germany Univ Manchester Manchester M13 9PL Lancs England

ISBN: (纸本)3540482814

In this paper we present a method of integrating theory reasoning into the instantiation framework. this integration is done in the black-box style, which allows us to integrate different theories in a uniform way. We prove completeness of the resulting calculus, provided that the theory reasoner is answer-complete and complete for reasoning with ground clauses. One of the distinctive features of our approach is that it allows us to employ off-the-shelf satisfiability solvers for ground clauses modulo theories, as a part of general first-order reasoning. As an application of this approach, we show how it is possible to combine the instantiation calculus with other calculi, such as ordered resolution and paramodulation.

关键词： Formal logic

来源：评论

学校读者我要写书评

暂无评论

An executable formalization of the HOL/Nuprl connection in the metalogical framework twelf

引用

13th international conference on logic for programming, Artificial Intelligence, and Reasoning

作者： Schurmann, Carsten Stehr, Mark-Oliver Yale Univ Dept Comp Sci New Haven CT 06520 USA Univ Illinois Siebel Ctr Comp Sci Urbana IL 61801 USA

ISBN: (纸本)3540482814

Howe's HOL/Nuprl connection is an interesting example of a translation between two fundamentally different logics, namely a typed higher-order logic and a polymorphic extensional type theory. In earlier work we have established a proof-theoretic correctness result of the translation in a way that complements Howe's semantics-based justification and furthermore goes beyond the original HOL/Nuprl connection by providing the foundation for a proof translator. Using the Twelf logical framework, the present paper goes one step further. It presents the first rigorous formalization of this treatment in a logical framework, and hence provides a safe alternative to the translation of proofs.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

Branching-time temporal logic extended with qualitative presburger constraints

引用

13th international conference on logic for programming, Artificial Intelligence, and Reasoning

作者： Bozzelli, Laura Gascon, Regis CNRS LSV Cachan France ENS Cachan Cachan France

ISBN: (纸本)3540482814

Recently, LTL extended with atomic formulas built over a constraint language interpreting variables in Z has been shown to have a decidable satisfiability and model-checking problem. this language allows to compare the variables at different states of the model and include periodicity constraints, comparison constraints, and a restricted form of quantification. On the other hand, the CTL counterpart of this logic (and hence also its CTL* counterpart which subsumes both LTL and CTL) has an undecidable model-checking problem. In this paper, we substantially extend the decidability border, by considering a meaningful fragment of CTL* extended with such constraints (which subsumes both the universal and existential fragments, as well as the EF-like fragment) and show that satisfiability and model-checking over relational automata that are abstraction of counter machines are decidable. the correctness and the termination of our algorithm rely on a suitable well quasi-ordering defined over the set of variable valuations.

关键词： logic programming

来源：评论

学校读者我要写书评

暂无评论

A local system for intuitionistic logic

引用

13th international conference on logic for programming, Artificial Intelligence, and Reasoning

作者： Tiu, Alwen Australian Natl Univ Canberra ACT Australia

ISBN: (纸本)3540482814

this paper presents systems for first-order intuitionistic logic and several of its extensions in which all the propositional rules are local, in the sense that, in applying the rules of the system, one needs only a fixed amount of information about the logical expressions involved. the main source of non-locality is the contraction rules. We show that the contraction rules can be restricted to the atomic ones, provided we employ deep-inference, i.e., to allow rules to apply anywhere inside logical expressions. We further show that the use of deep inference allows for modular extensions of intuitionistic logic to Dummett's intermediate logic LC, Godel logic and classical logic. We present the systems in the calculus of structures, a proof theoretic formalism which supports deep-inference. Cut elimination for these systems are proved indirectly by simulating the cut-free sequent systems, or the hypersequent systems in the cases of Dummett's LC and Godel logic, in the cut free systems in the calculus of structures.

关键词： proof theory intuitionistic logic intermediate logics deep inference calculus of structures locality

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：