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 | ||
| ||
Algorithmic decision theory : First International Conference, ADT 2009, Venice, Italy, October 20-23, 2009 ; Proceedings / / Francesca Rossi, Alexis Tsoukias (eds.)
| Algorithmic decision theory : First International Conference, ADT 2009, Venice, Italy, October 20-23, 2009 ; Proceedings / / Francesca Rossi, Alexis Tsoukias (eds.) |
| Edizione | [1st ed. 2009.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg, : Springer-Verlag, c2009 |
| Descrizione fisica | 1 online resource (XII, 460 p.) |
| Disciplina | 005.1 |
| Altri autori (Persone) |
RossiF (Francesca)
TsoukiasAlexis |
| Collana |
Lecture notes in artificial intelligence
Lecture notes in computer science |
| Soggetto topico |
Artificial intelligence
Automatic theorem proving Decision making - Data processing |
| ISBN | 3-642-04428-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Social Choice Theory -- A Complete Conclusion-Based Procedure for Judgment Aggregation -- A Geometric Approach to Paradoxes of Majority Voting in Abstract Aggregation Theory -- Manipulating Tournaments in Cup and Round Robin Competitions -- Iterated Majority Voting -- Committee Selection with a Weight Constraint Based on Lexicographic Rankings of Individuals -- The Effects of Noise and Manipulation on the Accuracy of Collective Decision Rules -- Subset Weight Maximization with Two Competing Agents -- The Complexity of Probabilistic Lobbying -- On the Complexity of Efficiency and Envy-Freeness in Fair Division of Indivisible Goods with Additive Preferences -- On Low-Envy Truthful Allocations -- On Multi-dimensional Envy-Free Mechanisms -- Stable Rankings in Collective Decision Making with Imprecise Information -- Finding Best k Policies -- Multiple Criteria Decision Analysis -- New Hybrid Recommender Approaches: An Application to Equity Funds Selection -- A Prescriptive Approach for Eliciting Imprecise Weight Statements in an MCDA Process -- Inverse Analysis from a Condorcet Robustness Denotation of Valued Outranking Relations -- Directional Decomposition of Multiattribute Utility Functions -- The Possible and the Necessary for Multiple Criteria Group Decision -- Preferences in an Open World -- Extending Argumentation to Make Good Decisions -- Building Consistent Pairwise Comparison Matrices over Abelian Linearly Ordered Groups -- Aggregating Interval Orders by Propositional Optimization -- Circular Representations of a Valued Preference Matrix -- Decision under Uncertainty -- The First Belief Dominance: A New Approach in Evidence Theory for Comparing Basic Belief Assignments -- Interpreting GUHA Data Mining Logic in Paraconsistent Fuzzy Logic Framework -- Insuring Risk-Averse Agents -- Adversarial Risk Analysis: Applications to Basic Counterterrorism Models -- Game Theory without Decision-Theoretic Paradoxes -- Ranking Methods Based on Dominance Measures Accounting for Imprecision -- Optimisation -- Optimizing the Hurwicz Criterion in Decision Trees with Imprecise Probabilities -- Axioms for a Class of Algorithms of Sequential Decision Making -- Algorithmic Aspects of Scenario-Based Multi-stage Decision Process Optimization -- Choquet Optimization Using GAI Networks for Multiagent/Multicriteria Decision-Making -- Compact Preference Representation in Stable Marriage Problems -- Neuroevolutionary Inventory Control in Multi-Echelon Systems -- Determining a Minimum Spanning Tree with Disjunctive Constraints -- Learning -- An Inductive Methodology for Data-Based Rules Building -- A Framework for Designing a Fuzzy Rule-Based Classifier -- Anytime Self-play Learning to Satisfy Functional Optimality Criteria. |
| Altri titoli varianti | ADT 2009 |
| Record Nr. | UNINA-9910484102003321 |
| Berlin ; ; Heidelberg, : Springer-Verlag, c2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated deduction : CADE-20 : 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005 : proceedings / / Robert Nieuwenhuis (ed.)
| Automated deduction : CADE-20 : 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005 : proceedings / / Robert Nieuwenhuis (ed.) |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, : Springer, 2005 |
| Descrizione fisica | 1 online resource (XIV, 466 p.) |
| Disciplina | 006.3 |
| Altri autori (Persone) | NieuwenhuisRobert |
| Collana | Lecture notes in artificial intelligence : a subseries of Lecture notes in computer science |
| Soggetto topico |
Automatic theorem proving
Logic, Symbolic and mathematical |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | What Do We Know When We Know That a Theory Is Consistent? -- Reflecting Proofs in First-Order Logic with Equality -- Reasoning in Extensional Type Theory with Equality -- Nominal Techniques in Isabelle/HOL -- Tabling for Higher-Order Logic Programming -- A Focusing Inverse Method Theorem Prover for First-Order Linear Logic -- The CoRe Calculus -- Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures -- Privacy-Sensitive Information Flow with JML -- The Decidability of the First-Order Theory of Knuth-Bendix Order -- Well-Nested Context Unification -- Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules -- The OWL Instance Store: System Description -- Temporal Logics over Transitive States -- Deciding Monodic Fragments by Temporal Resolution -- Hierarchic Reasoning in Local Theory Extensions -- Proof Planning for First-Order Temporal Logic -- System Description: Multi A Multi-strategy Proof Planner -- Decision Procedures Customized for Formal Verification -- An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic -- Connecting Many-Sorted Theories -- A Proof-Producing Decision Procedure for Real Arithmetic -- The MathSAT 3 System -- Deduction with XOR Constraints in Security API Modelling -- On the Complexity of Equational Horn Clauses -- A Combination Method for Generating Interpolants -- sKizzo: A Suite to Evaluate and Certify QBFs -- Regular Protocols and Attacks with Regular Knowledge -- The Model Evolution Calculus with Equality -- Model Representation via Contexts and Implicit Generalizations -- Proving Properties of Incremental Merkle Trees -- Computer Search for Counterexamples to Wilkie’s Identity -- KRHyper – In Your Pocket. |
| Altri titoli varianti |
Automated deduction : CADE-20
CADE-20 CADE-twenty 20th International Conference on Automated Deduction Twentieth International Conference on Automated Deduction International Conference on Automated Deduction CADE 2005 |
| Record Nr. | UNINA-9910483990803321 |
| Berlin, : Springer, 2005 | ||
| 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. | 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 | ||
| ||
