Logic for Programming, Artificial Intelligence, and Reasoning 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006. Proceedings /
| Συγγραφή απο Οργανισμό/Αρχή: | |
|---|---|
| Άλλοι συγγραφείς: | , |
| Μορφή: | Ηλεκτρονική πηγή Ηλ. βιβλίο |
| Γλώσσα: | English |
| Έκδοση: |
Berlin, Heidelberg :
Springer Berlin Heidelberg,
2006.
|
| Σειρά: | Lecture Notes in Computer Science,
4246 |
| Θέματα: | |
| Διαθέσιμο Online: | Full Text via HEAL-Link |
Πίνακας περιεχομένων:
- 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.
