Logic for Programming, Artificial Intelligence, and Reasoning : 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings / edited by Miki Hermann, Andrei Voronkov.

Format:

Book

Contributor:

Hermann, Miki, 1958- editor.

Voronkov, Andrei, 1959- editor.

SpringerLink (Online service)

Series:

Computer Science (Springer-11645)

Lecture notes in computer science. Lecture notes in artificial intelligence ; 4246.

Lecture Notes in Artificial Intelligence ; 4246

Language:

English

Subjects (All):

Artificial intelligence.

Computer programming.

Software engineering.

Computer logic.

Logic, Symbolic and mathematical.

Artificial Intelligence.

Programming Techniques.

Software Engineering.

Logics and Meanings of Programs.

Mathematical Logic and Formal Languages.

Local Subjects:

Artificial Intelligence.

Programming Techniques.

Software Engineering.

Logics and Meanings of Programs.

Mathematical Logic and Formal Languages.

Physical Description:

1 online resource (XIV, 592 pages).

Edition:

First edition 2006.

Contained In:

Springer eBooks

Place of Publication:

Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2006.

System Details:

text file PDF

Contents:

Higher-Order Termination: From Kruskal to Computability

Deciding Satisfiability of Positive Second Order Joinability Formulae

SAT Solving for Argument Filterings

Inductive Decidability Using Implicit Induction

Matching Modulo Superdevelopments Application to Second-Order Matching

Derivational Complexity of Knuth-Bendix Orders Revisited

A Characterization of Alternating Log Time by First Order Functional Programs

Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems

On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus

Modular Cut-Elimination: Finding Proofs or Counterexamples

An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf

A Semantic Completeness Proof for TaMeD

Saturation Up to Redundancy for Tableau and Sequent Calculi

Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints

Combining Supervaluation and Degree Based Reasoning Under Vagueness

A Comparison of Reasoning Techniques for Querying Large Description Logic ABoxes

A Local System for Intuitionistic Logic

CIC : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions

Reducing Nondeterminism in the Calculus of Structures

A Relaxed Approach to Integrity and Inconsistency in Databases

On Locally Checkable Properties

Deciding Key Cycles for Security Protocols

Automating Verification of Loops by Parallelization

On Computing Fixpoints in Well-Structured Regular Model Checking, with Applications to Lossy Channel Systems

Verification Condition Generation Via Theorem Proving

An Incremental Approach to Abstraction-Carrying Code

Context-Sensitive Multivariant Assertion Checking in Modular Programs

Representation of Partial Knowledge and Query Answering in Locally Complete Databases

Sequential, Parallel, and Quantified Updates of First-Order Structures

Representing Defaults and Negative Information Without Negation-as-Failure

Constructing Camin-Sokal Phylogenies Via Answer Set Programming

Automata for Positive Core XPath Queries on Compressed Documents

Boolean Rings for Intersection-Based Satisfiability

Theory Instantiation

Splitting on Demand in SAT Modulo Theories

Delayed Theory Combination vs. Nelson-Oppen for Satisfiability Modulo Theories: A Comparative Analysis

Automatic Combinability of Rewriting-Based Satisfiability Procedures

To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in

Lemma Learning in the Model Evolution Calculus.

Other Format:

Printed edition:

ISBN:

978-3-540-48282-6

9783540482826

Access Restriction:

Restricted for use by site license.