Automated Deduction — CADE-16 [electronic resource] : 16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 Proceedings /
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.
Main Authors: | , |
---|---|
Format: | Texto biblioteca |
Language: | eng |
Published: |
Berlin, Heidelberg : Springer Berlin Heidelberg,
1999
|
Subjects: | Computer science., Software engineering., Computer logic., Mathematical logic., Artificial intelligence., Computer Science., Artificial Intelligence (incl. Robotics)., Software Engineering/Programming and Operating Systems., Mathematical Logic and Formal Languages., Logics and Meanings of Programs., |
Online Access: | http://dx.doi.org/10.1007/3-540-48660-7 |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
KOHA-OAI-TEST:202100 |
---|---|
record_format |
koha |
spelling |
KOHA-OAI-TEST:2021002018-07-30T23:29:24ZAutomated Deduction — CADE-16 [electronic resource] : 16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 Proceedings / Ganzinger, Harald. author. SpringerLink (Online service) textBerlin, Heidelberg : Springer Berlin Heidelberg,1999.engSession 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.Computer science.Software engineering.Computer logic.Mathematical logic.Artificial intelligence.Computer Science.Artificial Intelligence (incl. Robotics).Software Engineering/Programming and Operating Systems.Mathematical Logic and Formal Languages.Logics and Meanings of Programs.Springer eBookshttp://dx.doi.org/10.1007/3-540-48660-7URN:ISBN:9783540486602 |
institution |
COLPOS |
collection |
Koha |
country |
México |
countrycode |
MX |
component |
Bibliográfico |
access |
En linea En linea |
databasecode |
cat-colpos |
tag |
biblioteca |
region |
America del Norte |
libraryname |
Departamento de documentación y biblioteca de COLPOS |
language |
eng |
topic |
Computer science. Software engineering. Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Artificial Intelligence (incl. Robotics). Software Engineering/Programming and Operating Systems. Mathematical Logic and Formal Languages. Logics and Meanings of Programs. Computer science. Software engineering. Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Artificial Intelligence (incl. Robotics). Software Engineering/Programming and Operating Systems. Mathematical Logic and Formal Languages. Logics and Meanings of Programs. |
spellingShingle |
Computer science. Software engineering. Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Artificial Intelligence (incl. Robotics). Software Engineering/Programming and Operating Systems. Mathematical Logic and Formal Languages. Logics and Meanings of Programs. Computer science. Software engineering. Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Artificial Intelligence (incl. Robotics). Software Engineering/Programming and Operating Systems. Mathematical Logic and Formal Languages. Logics and Meanings of Programs. Ganzinger, Harald. author. SpringerLink (Online service) Automated Deduction — CADE-16 [electronic resource] : 16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 Proceedings / |
description |
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. |
format |
Texto |
topic_facet |
Computer science. Software engineering. Computer logic. Mathematical logic. Artificial intelligence. Computer Science. Artificial Intelligence (incl. Robotics). Software Engineering/Programming and Operating Systems. Mathematical Logic and Formal Languages. Logics and Meanings of Programs. |
author |
Ganzinger, Harald. author. SpringerLink (Online service) |
author_facet |
Ganzinger, Harald. author. SpringerLink (Online service) |
author_sort |
Ganzinger, Harald. author. |
title |
Automated Deduction — CADE-16 [electronic resource] : 16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 Proceedings / |
title_short |
Automated Deduction — CADE-16 [electronic resource] : 16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 Proceedings / |
title_full |
Automated Deduction — CADE-16 [electronic resource] : 16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 Proceedings / |
title_fullStr |
Automated Deduction — CADE-16 [electronic resource] : 16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 Proceedings / |
title_full_unstemmed |
Automated Deduction — CADE-16 [electronic resource] : 16th International Conference on Automated Deduction Trento, Italy, July 7–10, 1999 Proceedings / |
title_sort |
automated deduction — cade-16 [electronic resource] : 16th international conference on automated deduction trento, italy, july 7–10, 1999 proceedings / |
publisher |
Berlin, Heidelberg : Springer Berlin Heidelberg, |
publishDate |
1999 |
url |
http://dx.doi.org/10.1007/3-540-48660-7 |
work_keys_str_mv |
AT ganzingerharaldauthor automateddeductioncade16electronicresource16thinternationalconferenceonautomateddeductiontrentoitalyjuly7101999proceedings AT springerlinkonlineservice automateddeductioncade16electronicresource16thinternationalconferenceonautomateddeductiontrentoitalyjuly7101999proceedings |
_version_ |
1756267654586302464 |