Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984 : proceedings / / edited by R. E. Shostak
| 7th International Conference on Automated Deduction, Napa, California, USA, May 14-16, 1984 : proceedings / / edited by R. E. Shostak |
| Edizione | [1st ed. 1984.] |
| Pubbl/distr/stampa | New York : , : Springer-Verlag, , [1984] |
| Descrizione fisica | 1 online resource (VIII, 509 p.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Automatic theorem proving
Logic, Symbolic and mathematical Computer science |
| ISBN | 0-387-34768-2 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Universal Unification -- A Portable Environment for Research in Automated Reasoning -- A Natural Proof System Based on Rewriting Techniques -- EKL—A Mathematically Oriented Proof Checker -- A Linear Characterization of NP-Complete Problems -- A Satisfiability Tester for Non-Clausal Propositional Calculus -- A Decision Method for Linear Temporal Logic -- A Progress Report on New Decision Algorithms for Finitely Presented Abelian Groups -- Canonical Forms in Finitely Presented Algebras -- Term Rewriting Systems and Algebra -- Termination of a Set of Rules Modulo a Set of Equations -- Associative-Commutative Unification -- A Linear Time Algorithm for a Subcase of Second Order Instantiation -- A New Equational Unification Method: A Generalisation of Martelli-Montanari’s Algorithm -- A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering that x 3 = x Implies Ring Commutativity -- A Narrowing Procedure for Theories with Constructors -- A General Inductive Completion Algorithm and Application to Abstract Data Types -- The Next Generation of Interactive Theorem Provers -- The Linked Inference Principle, II: The User’s Viewpoint -- A New Interpretation of the Resolution Principle -- Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving -- Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs -- Analytic and Non-analytic Proofs -- Applications of Protected Circumscription -- Implementation Strategies for Plan-Based Deduction -- A Programming Notation for Tactical Reasoning -- The Mechanization of Existence Proofs of Recursive Predicates -- Solving Word Problems in Free Algebras Using Complexity Functions -- Solving a Problem in Relevance Logic with an Automated Theorem Prover. |
| Record Nr. | UNISA-996465607703316 |
| New York : , : Springer-Verlag, , [1984] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated deduction - CADE-16 : 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, proceedings / / Harald Ganzinger (Ed.)
| Automated deduction - CADE-16 : 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, proceedings / / Harald Ganzinger (Ed.) |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (XIV, 438 p.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Automatic theorem proving |
| ISBN | 3-540-48660-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 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. |
| Record Nr. | UNINA-9910143461303321 |
| Berlin ; ; Heidelberg : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated deduction - CADE-16 : 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, proceedings / / Harald Ganzinger (Ed.)
| Automated deduction - CADE-16 : 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, proceedings / / Harald Ganzinger (Ed.) |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (XIV, 438 p.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Automatic theorem proving |
| ISBN | 3-540-48660-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 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. |
| Record Nr. | UNISA-996465753503316 |
| Berlin ; ; Heidelberg : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated deduction - CADE-21 : 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007 : proceedings / / Frank Pfenning
| Automated deduction - CADE-21 : 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007 : proceedings / / Frank Pfenning |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Germany ; ; New York, New York : , : Springer, , [2007] |
| Descrizione fisica | 1 online resource (XII, 524 p.) |
| Disciplina | 511.3 |
| Collana | Lecture notes in computer science,Lecture notes in artificial intelligence |
| Soggetto topico |
Automatic theorem proving
Logic, Symbolic and mathematical |
| ISBN | 3-540-73595-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Session 1. Invited Talk: Colin Stirling -- Games, Automata and Matching -- Session 2. Higher-Order Logic -- Formalization of Continuous Probability Distributions -- Compilation as Rewriting in Higher Order Logic -- Barendregt’s Variable Convention in Rule Inductions -- Automating Elementary Number-Theoretic Proofs Using Gröbner Bases -- Session 3. Description Logic -- Optimized Reasoning in Description Logics Using Hypertableaux -- Conservative Extensions in the Lightweight Description Logic -- An Incremental Technique for Automata-Based Decision Procedures -- Session 4. Intuitionistic Logic -- Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4 -- A Labelled System for IPL with Variable Splitting -- Session 5. Invited Talk: Ashish Tiwari -- Logical Interpretation: Static Program Analysis Using Theorem Proving -- Session 6. Satisfiability Modulo Theories -- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories -- Efficient E-Matching for SMT Solvers -- -Decision by Decomposition -- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic -- Session 7. Induction, Rewriting, and Polymorphism -- Improvements in Formula Generalization -- On the Normalization and Unique Normalization Properties of Term Rewrite Systems -- Handling Polymorphism in Automated Deduction -- Session 8. First-Order Logic -- Automated Reasoning in Kleene Algebra -- SRASS - A Semantic Relevance Axiom Selection System -- Labelled Clauses -- Automatic Decidability and Combinability Revisited -- Session 9. Invited Talk: K. Rustan M. Leino -- Designing Verification Conditions for Software -- Session 10. Model Checking and Verification -- Encodings of Bounded LTL Model Checking in Effectively Propositional Logic -- Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems -- The KeY system 1.0 (Deduction Component) -- KeY-C: A Tool for Verification of C Programs -- The Bedwyr System for Model Checking over Syntactic Expressions -- System for Automated Deduction (SAD): A Tool for Proof Verification -- Session 11. Invited Talk: Peter Baumgartner -- Logical Engineering with Instance-Based Methods -- Session 12. Termination -- Predictive Labeling with Dependency Pairs Using SAT -- Dependency Pairs for Rewriting with Non-free Constructors -- Proving Termination by Bounded Increase -- Certified Size-Change Termination -- Session 13. Tableaux and First-Order Systems -- Encoding First Order Proofs in SAT -- Hyper Tableaux with Equality -- System Description: E- KRHyper -- System Description: Spass Version 3.0. |
| Record Nr. | UNINA-9910484284303321 |
| Berlin, Germany ; ; New York, New York : , : Springer, , [2007] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated deduction - CADE-21 : 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007 : proceedings / / Frank Pfenning
| Automated deduction - CADE-21 : 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007 : proceedings / / Frank Pfenning |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Germany ; ; New York, New York : , : Springer, , [2007] |
| Descrizione fisica | 1 online resource (XII, 524 p.) |
| Disciplina | 511.3 |
| Collana | Lecture notes in computer science,Lecture notes in artificial intelligence |
| Soggetto topico |
Automatic theorem proving
Logic, Symbolic and mathematical |
| ISBN | 3-540-73595-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Session 1. Invited Talk: Colin Stirling -- Games, Automata and Matching -- Session 2. Higher-Order Logic -- Formalization of Continuous Probability Distributions -- Compilation as Rewriting in Higher Order Logic -- Barendregt’s Variable Convention in Rule Inductions -- Automating Elementary Number-Theoretic Proofs Using Gröbner Bases -- Session 3. Description Logic -- Optimized Reasoning in Description Logics Using Hypertableaux -- Conservative Extensions in the Lightweight Description Logic -- An Incremental Technique for Automata-Based Decision Procedures -- Session 4. Intuitionistic Logic -- Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4 -- A Labelled System for IPL with Variable Splitting -- Session 5. Invited Talk: Ashish Tiwari -- Logical Interpretation: Static Program Analysis Using Theorem Proving -- Session 6. Satisfiability Modulo Theories -- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories -- Efficient E-Matching for SMT Solvers -- -Decision by Decomposition -- Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic -- Session 7. Induction, Rewriting, and Polymorphism -- Improvements in Formula Generalization -- On the Normalization and Unique Normalization Properties of Term Rewrite Systems -- Handling Polymorphism in Automated Deduction -- Session 8. First-Order Logic -- Automated Reasoning in Kleene Algebra -- SRASS - A Semantic Relevance Axiom Selection System -- Labelled Clauses -- Automatic Decidability and Combinability Revisited -- Session 9. Invited Talk: K. Rustan M. Leino -- Designing Verification Conditions for Software -- Session 10. Model Checking and Verification -- Encodings of Bounded LTL Model Checking in Effectively Propositional Logic -- Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems -- The KeY system 1.0 (Deduction Component) -- KeY-C: A Tool for Verification of C Programs -- The Bedwyr System for Model Checking over Syntactic Expressions -- System for Automated Deduction (SAD): A Tool for Proof Verification -- Session 11. Invited Talk: Peter Baumgartner -- Logical Engineering with Instance-Based Methods -- Session 12. Termination -- Predictive Labeling with Dependency Pairs Using SAT -- Dependency Pairs for Rewriting with Non-free Constructors -- Proving Termination by Bounded Increase -- Certified Size-Change Termination -- Session 13. Tableaux and First-Order Systems -- Encoding First Order Proofs in SAT -- Hyper Tableaux with Equality -- System Description: E- KRHyper -- System Description: Spass Version 3.0. |
| Record Nr. | UNISA-996465915403316 |
| Berlin, Germany ; ; New York, New York : , : Springer, , [2007] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated deduction - CADE-22 : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 : proceedings / / Renate A. Schmidt
| Automated deduction - CADE-22 : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 : proceedings / / Renate A. Schmidt |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Germany ; ; New York, New York : , : Springer, , [2009] |
| Descrizione fisica | 1 online resource (515 p.) |
| Disciplina | 006.3 |
| Collana |
Lecture notes in computer science
Lecture notes in artificial intelligence LNCS sublibrary. SL 7, Artificial intelligence |
| Soggetto topico |
Logic, Symbolic and mathematical
Automatic theorem proving |
| ISBN |
1-282-33197-3
9786612331978 3-642-02959-0 |
| Classificazione |
DAT 706f
DAT 716f SS 4800 004 510 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Session 1. Invited Talk -- Integrated Reasoning and Proof Choice Point Selection in the Jahob System – Mechanisms for Program Survival -- Session 2. Combinations and Extensions -- Superposition and Model Evolution Combined -- On Deciding Satisfiability by DPLL( ) and Unsound Theorem Proving -- Combinable Extensions of Abelian Groups -- Locality Results for Certain Extensions of Theories with Bridging Functions -- Session 3. Minimal Unsatisfiability and Automated Reasoning Support -- Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis -- Does This Set of Clauses Overlap with at Least One MUS? -- Progress in the Development of Automated Theorem Proving for Higher-Order Logic -- Session 4. System Descriptions -- System Description: H-PILoT -- SPASS Version 3.5 -- Dei: A Theorem Prover for Terms with Integer Exponents -- veriT: An Open, Trustable and Efficient SMT-Solver -- Divvy: An ATP Meta-system Based on Axiom Relevance Ordering -- Session 5. Invited Talk -- Instantiation-Based Automated Reasoning: From Theory to Practice -- Session 6. Interpolation and Predicate Abstraction -- Interpolant Generation for UTVPI -- Ground Interpolation for Combined Theories -- Interpolation and Symbol Elimination -- Complexity and Algorithms for Monomial and Clausal Predicate Abstraction -- Session 7. Resolution-Based Systems for Non-classical Logics -- Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method -- A Refined Resolution Calculus for CTL -- Fair Derivations in Monodic Temporal Reasoning -- Session 8. Termination Analysis and Constraint Solving -- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs -- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic -- Session 9. Invited Talk -- Building Theorem Provers -- Session 10. Rewriting, Termination and Productivity -- Termination Analysis by Dependency Pairs and Inductive Theorem Proving -- Beyond Dependency Graphs -- Computing Knowledge in Security Protocols under Convergent Equational Theories -- Complexity of Fractran and Productivity -- Session 11. Models -- Automated Inference of Finite Unsatisfiability -- Decidability Results for Saturation-Based Model Building -- Session 12. Modal Tableaux with Global Caching -- A Tableau Calculus for Regular Grammar Logics with Converse -- An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability -- Session 13. Arithmetic -- Volume Computation for Boolean Combination of Linear Arithmetic Constraints -- A Generalization of Semenov’s Theorem to Automata over Real Numbers -- Real World Verification. |
| Altri titoli varianti | CADE 22 |
| Record Nr. | UNINA-9910483050003321 |
| Berlin, Germany ; ; New York, New York : , : Springer, , [2009] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated deduction - CADE-22 : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 : proceedings / / Renate A. Schmidt
| Automated deduction - CADE-22 : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 : proceedings / / Renate A. Schmidt |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin, Germany ; ; New York, New York : , : Springer, , [2009] |
| Descrizione fisica | 1 online resource (515 p.) |
| Disciplina | 006.3 |
| Collana |
Lecture notes in computer science
Lecture notes in artificial intelligence LNCS sublibrary. SL 7, Artificial intelligence |
| Soggetto topico |
Logic, Symbolic and mathematical
Automatic theorem proving |
| ISBN |
1-282-33197-3
9786612331978 3-642-02959-0 |
| Classificazione |
DAT 706f
DAT 716f SS 4800 004 510 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Session 1. Invited Talk -- Integrated Reasoning and Proof Choice Point Selection in the Jahob System – Mechanisms for Program Survival -- Session 2. Combinations and Extensions -- Superposition and Model Evolution Combined -- On Deciding Satisfiability by DPLL( ) and Unsound Theorem Proving -- Combinable Extensions of Abelian Groups -- Locality Results for Certain Extensions of Theories with Bridging Functions -- Session 3. Minimal Unsatisfiability and Automated Reasoning Support -- Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis -- Does This Set of Clauses Overlap with at Least One MUS? -- Progress in the Development of Automated Theorem Proving for Higher-Order Logic -- Session 4. System Descriptions -- System Description: H-PILoT -- SPASS Version 3.5 -- Dei: A Theorem Prover for Terms with Integer Exponents -- veriT: An Open, Trustable and Efficient SMT-Solver -- Divvy: An ATP Meta-system Based on Axiom Relevance Ordering -- Session 5. Invited Talk -- Instantiation-Based Automated Reasoning: From Theory to Practice -- Session 6. Interpolation and Predicate Abstraction -- Interpolant Generation for UTVPI -- Ground Interpolation for Combined Theories -- Interpolation and Symbol Elimination -- Complexity and Algorithms for Monomial and Clausal Predicate Abstraction -- Session 7. Resolution-Based Systems for Non-classical Logics -- Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method -- A Refined Resolution Calculus for CTL -- Fair Derivations in Monodic Temporal Reasoning -- Session 8. Termination Analysis and Constraint Solving -- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs -- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic -- Session 9. Invited Talk -- Building Theorem Provers -- Session 10. Rewriting, Termination and Productivity -- Termination Analysis by Dependency Pairs and Inductive Theorem Proving -- Beyond Dependency Graphs -- Computing Knowledge in Security Protocols under Convergent Equational Theories -- Complexity of Fractran and Productivity -- Session 11. Models -- Automated Inference of Finite Unsatisfiability -- Decidability Results for Saturation-Based Model Building -- Session 12. Modal Tableaux with Global Caching -- A Tableau Calculus for Regular Grammar Logics with Converse -- An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability -- Session 13. Arithmetic -- Volume Computation for Boolean Combination of Linear Arithmetic Constraints -- A Generalization of Semenov’s Theorem to Automata over Real Numbers -- Real World Verification. |
| Altri titoli varianti | CADE 22 |
| Record Nr. | UNISA-996465837603316 |
| Berlin, Germany ; ; New York, New York : , : Springer, , [2009] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated deduction in geometry : 6th International Workshop, ADG 2006, Pontevedra, Spain, August 31-September 2, 2006, Revised Papers : 6th International Workshop, ADG 2006, Pontevedra, Spain, August 31-September 2, 2006, revised papers / / Francisco Botana, Tomas Recio (Eds.)
| Automated deduction in geometry : 6th International Workshop, ADG 2006, Pontevedra, Spain, August 31-September 2, 2006, Revised Papers : 6th International Workshop, ADG 2006, Pontevedra, Spain, August 31-September 2, 2006, revised papers / / Francisco Botana, Tomas Recio (Eds.) |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer, , [2007] |
| Descrizione fisica | 1 online resource (X, 218 p.) |
| Disciplina | 516.00285 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Geometry - Data processing
Automatic theorem proving |
| ISBN | 3-540-77356-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Towards an Electronic Geometry Textbook -- Equidecomposable Quadratic Regions -- Automatic Verification of Regular Constructions in Dynamic Geometry Systems -- Recognition of Computationally Constructed Loci -- Algorithmic Search for Flexibility Using Resultants of Polynomial Systems -- Cylinders Through Five Points: Complex and Real Enumerative Geometry -- Detecting All Dependences in Systems of Geometric Constraints Using the Witness Method -- Automatic Discovery of Geometry Theorems Using Minimal Canonical Comprehensive Gröbner Systems -- Mechanical Theorem Proving in Tarski’s Geometry -- On the Need of Radical Ideals in Automatic Proving: A Theorem About Regular Polygons -- A Maple Package for Automatic Theorem Proving and Discovery in 3D-Geometry -- Geometry Expressions: A Constraint Based Interactive Symbolic Geometry System -- Constructing a Tetrahedron with Prescribed Heights and Widths. |
| Record Nr. | UNINA-9910483640303321 |
| Berlin ; ; Heidelberg : , : Springer, , [2007] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated deduction in geometry : 6th International Workshop, ADG 2006, Pontevedra, Spain, August 31-September 2, 2006, Revised Papers : 6th International Workshop, ADG 2006, Pontevedra, Spain, August 31-September 2, 2006, revised papers / / Francisco Botana, Tomas Recio (Eds.)
| Automated deduction in geometry : 6th International Workshop, ADG 2006, Pontevedra, Spain, August 31-September 2, 2006, Revised Papers : 6th International Workshop, ADG 2006, Pontevedra, Spain, August 31-September 2, 2006, revised papers / / Francisco Botana, Tomas Recio (Eds.) |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer, , [2007] |
| Descrizione fisica | 1 online resource (X, 218 p.) |
| Disciplina | 516.00285 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Geometry - Data processing
Automatic theorem proving |
| ISBN | 3-540-77356-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Towards an Electronic Geometry Textbook -- Equidecomposable Quadratic Regions -- Automatic Verification of Regular Constructions in Dynamic Geometry Systems -- Recognition of Computationally Constructed Loci -- Algorithmic Search for Flexibility Using Resultants of Polynomial Systems -- Cylinders Through Five Points: Complex and Real Enumerative Geometry -- Detecting All Dependences in Systems of Geometric Constraints Using the Witness Method -- Automatic Discovery of Geometry Theorems Using Minimal Canonical Comprehensive Gröbner Systems -- Mechanical Theorem Proving in Tarski’s Geometry -- On the Need of Radical Ideals in Automatic Proving: A Theorem About Regular Polygons -- A Maple Package for Automatic Theorem Proving and Discovery in 3D-Geometry -- Geometry Expressions: A Constraint Based Interactive Symbolic Geometry System -- Constructing a Tetrahedron with Prescribed Heights and Widths. |
| Record Nr. | UNISA-996465914703316 |
| Berlin ; ; Heidelberg : , : Springer, , [2007] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated deduction in geometry : Second International Workshop, ADG '98, Beijing, China, August 1998 : proceedings / / Xiao-Shan Gao, Dongming Wang, Lu Yang, editors
| Automated deduction in geometry : Second International Workshop, ADG '98, Beijing, China, August 1998 : proceedings / / Xiao-Shan Gao, Dongming Wang, Lu Yang, editors |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (VIII, 292 p.) |
| Disciplina | 516.00285 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Geometry - Data processing
Automatic theorem proving |
| ISBN | 3-540-47997-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Automatic Geometry Theorem-Proving and Automatic Geometry Problem-Solving -- Solving Geometric Problems with Real Quantifier Elimination -- Automated Discovering and Proving for Geometric Inequalities -- Proving Newton’s Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle -- Readable Machine Solving in Geometry and ICAI Software MSG -- Plane Euclidean Reasoning -- A Clifford Algebraic Method for Geometric Reasoning -- Clifford Term Rewriting for Geometric Reasoning in 3D -- Some Applications of Clifford Algebra to Geometries -- Decomposing Algebraic Varieties -- An Application of Automatic Theorem Proving in Computer Vision -- Automated Geometry Diagram Construction and Engineering Geometry -- A 2D Geometric Constraint Solver for Parametric Design Using Graph Analysis and Reduction -- Variant Geometry Analysis and Synthesis in Mechanical CAD. |
| Record Nr. | UNISA-996465597603316 |
| Berlin ; ; Heidelberg : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
