用分析表格与有关方法自动推理/会议录 Automated reasoning with analytic tableaux and related methods

作者： Pieter Adriaans著

出 版 社： 湖南文艺出版社

出版时间： 2002-12-1字数：版次： 1页数： 339印刷时间： 2002/12/01开本：印次：纸张： 胶版纸I S B N ： 9783540439295包装： 平装编辑推荐

LNBI is devoted to the publication of state-of-the-art research results in bio-informatics and computational biology, at a high level and in both printed and electronic versions - making use of the well-established LNCS publication machinery. As with the LNCS mother series, refereed proceedings and post- proceedings are at the core of LNBI, however, similar to the color cover sub- lines in LNCS, tutorials and state-of-the-art surveys are also invited for LNBI. Among the topics covered are：

Genomics；Molecular sequence analysis；Recognition of genes and regulatory elements；Molecular evolution；Protein structure；Gene expression；Gene networks；Combinatorial libraries and drug design；Computational proteomics.

内容简介

This book constitutes the refereed proceedings of the 6th International Colloquium on Grammatical Inference, ICGI 2002, held in Amsterdam, The Netherlands in September 2002.The 28 revised full papers presented together with 7 software descriptions were carefully reviewed and selected from 48 submissions. The papers address issues in machine learning, automata, theoretical computer science, computational linguistics, and grammar systems as well as applications in fields like natural language processing, pattern recognition, computational biology, information retrieval, text processing, and data compression.

目录

Invited Papers

Proof Analysis by Resolution

Using Linear Logic to Reason about Sequent Systems

Research Papers

A Schiitte-Tait Style Cut-Elimination Proof for First-OrderGSdel Logic

Tableaux for Quantified Hybrid Logic

Tableau-Based Automated Deduction for Duration Calculus

Linear Time Logic, Conditioned Models, and Planning withIncomplete Knowledge

A Simplified Clausal Resolution Procedure for PropositionalLinear-Time Temporal Logic

Modal Nonmonotonic Logics Revisited: Efficient Encodings for theBasic Reasoning Tasks

Tableau Calculi for the Logics of Finite k-Ary Trees

A Model Generation Style Completeness Proof for ConstraintTableaux with Superposition

Implementation and Optimisation of a Tableau Algorithm for theGuarded Fragment

Lemma and Model Caching in Decision Procedures for QuantifiedBoolean Formulas

Integration of Equality Reasoning into the Disconnection Calculus

Analytic Sequent Calculi for Abelian and Lukasiewicz Logics

Analytic Tableau Systems for Propositional Bimodal Logics ofKnowledge and Belief

A Confluent Theory Connection Calculus

On Uniform Word Problems Involving Bridging Operators onDistributive Lattices

Question Answering: From Partitions to Prolog

A General Theorem Prover for Quantified Modal Logics

Some New Exceptions for the Semantic Tableaux Version ofthe Second Incompleteness Theorem

A New Indefinite Semantics for Hilbert's Epsilon

A Tableau Calculus for Combining Non-disjoint Theories

System Descriptions Papers

LINK: A Proof Environment Based on Proof Nets

DCTP 1.2 - System Abstract

Author Index