Automated Deduction - CADE-16 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings /

Automated Deduction - CADE-16 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings /

Λεπτομέρειες βιβλιογραφικής εγγραφής
Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
Άλλοι συγγραφείς: Ganzinger, Harald (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
Γλώσσα:English
Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1999.
Έκδοση:1st ed. 1999.
Σειρά:Lecture Notes in Artificial Intelligence ; 1632
Θέματα:
Artificial intelligence.
Software engineering.
Mathematical logic.
Computer logic.
Artificial Intelligence.
Software Engineering/Programming and Operating Systems.
Mathematical Logic and Formal Languages.
Logics and Meanings of Programs.
Διαθέσιμο Online:Full Text via HEAL-Link
Πίνακας περιεχομένων:
  • Session 1
  • A Dynamic Programming Approach to Categorial Deduction
  • Tractable Transformations from Modal Provability Logics into First-Order Logic
  • Session 2
  • Decision Procedures for Guarded Logics
  • A PSpace Algorithm for Graded Modal Logic
  • Session 3
  • Solvability of Context Equations with Two Context Variables Is Decidable
  • Complexity of the Higher Order Matching
  • Solving Equational Problems Efficiently
  • Session 4
  • VSDITLU: A Verifiable Symbolic Definite Integral Table Look-Up
  • A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers
  • Presenting Proofs in a Human-Oriented Way
  • Session 5
  • On the Universal Theory of Varieties of Distributive Lattices with Operators: Some Decidability and Complexity Results
  • Maslov's Class K Revisited
  • Prefixed Resolution: A Resolution Method for Modal and Description Logics
  • Session 6: System Descriptions
  • System Description: Twelf - A Meta-Logical Framework for Deductive Systems
  • System Description: inka 5.0 - A Logic Voyager
  • System Description: CutRes 0.1: Cut Elimination by Resolution
  • System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving
  • System Description Using OBDD's for the Validationof Skolem Verification Conditions
  • Fault-Tolerant Distributed Theorem Proving
  • System Description: Waldmeister - Improvements in Performance and Ease of Use
  • Session 7
  • Formal Metatheory Using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems
  • A Formalization of Static Analyses in System F
  • On Explicit Reflection in Theorem Proving and Formal Verification
  • Session 8: System Descriptions
  • System Description: Kimba, A Model Generator for Many-Valued First-Order Logics
  • System Description: Teyjus-A Compiler and Abstract Machine Based Implementation of ?Prolog
  • Vampire
  • System Abstract: E 0.3
  • Session 9
  • Invited Talk: Rewrite-Based Deduction and Symbolic Constraints
  • Towards an Automatic Analysis of Security Protocols in First-Order Logic
  • Session 10
  • A Confluent Connection Calculus
  • Abstraction-Based Relevancy Testing for Model Elimination
  • A Breadth-First Strategy for Mating Search
  • Session 11: System Competitions
  • The Design of the CADE-16 Inductive Theorem Prover Contest
  • Session 12: System Descriptions
  • System Description: Spass Version 1.0.0
  • K : A Theorem Prover for K
  • System Description: CYNTHIA
  • System Description: MCS: Model-Based Conjecture Searching
  • Session 13
  • Embedding Programming Languages in Theorem Provers
  • Extensional Higher-Order Paramodulation and RUE-Resolution
  • Automatic Generation of Proof Search Strategies for Second-Order Logic.

Παρόμοια τεκμήρια