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.
Logic for programming, artificial intelligence, and reasoning : 14th international conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007 : proceedings / / Nachum Dershowitz, Andrei Voronkov (eds.)
| Logic for programming, artificial intelligence, and reasoning : 14th international conference, LPAR 2007, Yerevan, Armenia, October 15-19, 2007 : proceedings / / Nachum Dershowitz, Andrei Voronkov (eds.) |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2007 |
| Descrizione fisica | 1 online resource (XIII, 564 p.) |
| Disciplina | 006.3 |
| Altri autori (Persone) |
DershowitzNachum
VoronkovA <1959-> (Andrei) |
| Collana |
LNCS sublibrary. SL 7, Artificial intelligence
Lectures notes in computer science. Lecture notes in artificial intelligence |
| Soggetto topico |
Logic programming
Artificial intelligence Automatic theorem proving |
| ISBN | 3-540-75560-8 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | From Hilbert’s Program to a Logic Toolbox -- On the Notion of Vacuous Truth -- Whatever Happened to Deductive Question Answering? -- Decidable Fragments of Many-Sorted Logic -- One-Pass Tableaux for Computation Tree Logic -- Extending a Resolution Prover for Inequalities on Elementary Functions -- Model Checking the First-Order Fragment of Higher-Order Fixpoint Logic -- Monadic Fragments of Gödel Logics: Decidability and Undecidability Results -- Least and Greatest Fixed Points in Linear Logic -- The Semantics of Consistency and Trust in Peer Data Exchange Systems -- Completeness and Decidability in Sequence Logic -- HORPO with Computability Closure: A Reconstruction -- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs -- Matching in Hybrid Terminologies -- Verifying Cryptographic Protocols with Subterms Constraints -- Deciding Knowledge in Security Protocols for Monoidal Equational Theories -- Mechanized Verification of CPS Transformations -- Operational and Epistemic Approaches to Protocol Analysis: Bridging the Gap -- Protocol Verification Via Rigid/Flexible Resolution -- Preferential Description Logics -- On Two Extensions of Abstract Categorial Grammars -- Why Would You Trust B? -- How Many Legs Do I Have? Non-Simple Roles in Number Restrictions Revisited -- On Finite Satisfiability of the Guarded Fragment with Equivalence or Transitive Guards -- Data Complexity in the Family of Description Logics -- An Extension of the Knuth-Bendix Ordering with LPO-Like Properties -- Retractile Proof Nets of the Purely Multiplicative and Additive Fragment of Linear Logic -- Integrating Inductive Definitions in SAT -- The Separation Theorem for Differential Interaction Nets -- Complexity of Planning in Action Formalisms Based on Description Logics -- Faster Phylogenetic Inference with MXG -- Enriched ?–Calculus Pushdown Module Checking -- Approved Models for Normal Logic Programs -- Permutative Additives and Exponentials -- Algorithms for Propositional Model Counting -- Completeness for Flat Modal Fixpoint Logics -- : Decidable Non-monotonic Disjunctive Logic Programs with Function Symbols -- The Complexity of Temporal Logic with Until and Since over Ordinals -- ATP Cross-Verification of the Mizar MPTP Challenge Problems. |
| Altri titoli varianti | LPAR 2007 |
| Record Nr. | UNINA-9910768439603321 |
| Berlin ; ; New York, : Springer, c2007 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Logic for programming, artificial intelligence, and reasoning : 13th international conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006 : proceedings / / Miki Hermann, Andrei Voronkov (eds.)
| Logic for programming, artificial intelligence, and reasoning : 13th international conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006 : proceedings / / Miki Hermann, Andrei Voronkov (eds.) |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2006 |
| Descrizione fisica | 1 online resource (XIV, 592 p.) |
| Disciplina | 006.3 |
| Altri autori (Persone) |
HermannMiki <1958->
VoronkovA <1959-> (Andrei) |
| Collana |
LNCS sublibrary. SL 7, Artificial intelligence
Lecture notes in computer science,Lecture notes in artificial intelligence |
| Soggetto topico |
Logic programming
Automatic theorem proving Artificial intelligence |
| ISBN | 3-540-48282-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 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. |
| Altri titoli varianti | LPAR 2006 |
| Record Nr. | UNINA-9910484466603321 |
| Berlin ; ; New York, : Springer, c2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Logic for programming, artificial intelligence, and reasoning : 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005 : proceedings / / Geoff Sutcliffe, Andrei Voronkov (eds.)
| Logic for programming, artificial intelligence, and reasoning : 12th international conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005 : proceedings / / Geoff Sutcliffe, Andrei Voronkov (eds.) |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2005 |
| Descrizione fisica | 1 online resource (XIV, 744 p.) |
| Disciplina | 005.1/15 |
| Altri autori (Persone) |
SutcliffeGeoff
VoronkovA <1959-> (Andrei) |
| Collana | Lecture notes in computer science,Lecture notes in artificial intelligence |
| Soggetto topico |
Logic programming
Automatic theorem proving Artificial intelligence |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Independently Checkable Proofs from Decision Procedures: Issues and Progress -- Zap: Automated Theorem Proving for Software Analysis -- Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools -- Scaling Up: Computers vs. Common Sense -- A New Constraint Solver for 3D Lattices and Its Application to the Protein Folding Problem -- Disjunctive Constraint Lambda Calculi -- Computational Issues in Exploiting Dependent And-Parallelism in Logic Programming: Leftness Detection in Dynamic Search Trees -- The nomore?+?+ Approach to Answer Set Solving -- Optimizing the Runtime Processing of Types in Polymorphic Logic Programming Languages -- The Four Sons of Penrose -- An Algorithmic Account of Ehrenfeucht Games on Labeled Successor Structures -- Second-Order Principles in Specification Languages for Object-Oriented Programs -- Strong Normalization of the Dual Classical Sequent Calculus -- Termination of Fair Computations in Term Rewriting -- On Confluence of Infinitary Combinatory Reduction Systems -- Matching with Regular Constraints -- Recursive Path Orderings Can Also Be Incremental -- Automating Coherent Logic -- The Theorema Environment for Interactive Proof Development -- A First Order Extension of Stålmarck’s Method -- Regular Derivations in Basic Superposition-Based Calculi -- On the Finite Satisfiability Problem for the Guarded Fragment with Transitivity -- Deciding Separation Logic Formulae by SAT and Incremental Negative Cycle Elimination -- Monotone AC-Tree Automata -- On the Specification of Sequent Systems -- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic -- Integration of a Software Model Checker into Isabelle -- Experimental Evaluation of Classical Automata Constructions -- Automatic Validation of Transformation Rules for Java Verification Against a Rewriting Semantics -- Reasoning About Incompletely Defined Programs -- Model Checking Abstract State Machines with Answer Set Programming -- Characterizing Provability in BI’s Pointer Logic Through Resource Graphs -- A Unified Memory Model for Pointers -- Treewidth in Verification: Local vs. Global -- Pushdown Module Checking -- Functional Correctness Proofs of Encryption Algorithms -- Towards Automated Proof Support for Probabilistic Distributed Systems -- Algebraic Intruder Deductions -- Satisfiability Checking for PC(ID) -- Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning -- Another Complete Local Search Method for SAT -- Inference from Controversial Arguments -- Programming Cognitive Agents in Defeasible Logic -- The Relationship Between Reasoning About Privacy and Default Logics -- Comparative Similarity, Tree Automata, and Diophantine Equations -- Analytic Tableaux for KLM Preferential and Cumulative Logics -- Bounding Resource Consumption with Gödel-Dummett Logics -- On Interpolation in Existence Logics -- Incremental Integrity Checking: Limitations and Possibilities -- Concepts of Automata Construction from LTL. |
| Altri titoli varianti | LPAR 2005 |
| Record Nr. | UNINA-9910483264503321 |
| Berlin ; ; New York, : Springer, c2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Logic for programming, artificial intelligence, and reasoning : 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005 : proceedings / / Franz Baader, Andrei Voronkov (eds.)
| Logic for programming, artificial intelligence, and reasoning : 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005 : proceedings / / Franz Baader, Andrei Voronkov (eds.) |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2005 |
| Descrizione fisica | 1 online resource (XII, 560 p.) |
| Disciplina | 005.1/15 |
| Altri autori (Persone) |
BaaderFranz
VoronkovA <1959-> (Andrei) |
| Collana | Lecture notes in computer science,Lecture notes in artificial intelligence |
| Soggetto topico |
Logic programming
Automatic theorem proving Artificial intelligence |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | CERES in Many-Valued Logics -- A Decomposition Rule for Decision Procedures by Resolution-Based Calculi -- Abstract DPLL and Abstract DPLL Modulo Theories -- Combining Lists with Non-stably Infinite Theories -- Abstract Model Generation for Preprocessing Clause Sets -- Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying -- Applications of General Exact Satisfiability in Propositional Logic Modelling -- BCiC: A System for Code Authentication and Verification -- Ordered Resolution with Selection for -- On a Semantic Subsumption Test -- Suitable Graphs for Answer Set Programming -- Weighted Answer Sets and Applications in Intelligence Analysis -- How to Fix It: Using Fixpoints in Different Contexts -- Reasoning About Systems with Transition Fairness -- Entanglement – A Measure for the Complexity of Directed Graphs with Applications to Logic and Games -- How the Location of * Influences Complexity in Kleene Algebra with Tests -- The Equational Theory of ??, 0, 1,?+?, ×, ?? Is Decidable, but Not Finitely Axiomatisable -- A Trichotomy in the Complexity of Propositional Circumscription -- Exploiting Fixable, Removable, and Implied Values in Constraint Satisfaction Problems -- Evaluating QBFs via Symbolic Skolemization -- The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs -- Automated Termination Analysis for Incompletely Defined Programs -- Automatic Certification of Heap Consumption -- A Formalization of Off-Line Guessing for Security Protocol Analysis -- Abstraction-Carrying Code -- A Verification Environment for Sequential Imperative Programs in Isabelle/HOL -- Can a Higher-Order and a First-Order Theorem Prover Cooperate? -- A Generic Framework for Interprocedural Analyses of Numerical Properties -- Second-Order Matching via Explicit Substitutions -- Knowledge-Based Synthesis of Distributed Systems Using Event Structures -- The Inverse Method for the Logic of Bunched Implications -- Cut-Elimination: Experiments with CERES -- Uniform Rules and Dialogue Games for Fuzzy Logics -- Nonmonotonic Description Logic Programs: Implementation and Experiments -- Implementing Efficient Resource Management for Linear Logic Programming -- Layered Clausal Resolution in the Multi-modal Logic of Beliefs and Goals. |
| Altri titoli varianti | LPAR 2004 |
| Record Nr. | UNINA-9910484247503321 |
| Berlin ; ; New York, : Springer, c2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Mathematical knowledge management : 5th international conference, MKM 2006, Wokingham, UK, August 11-12, 2006 : proceedings / / Jonathan M. Borwein, William M. Farmer (eds.)
| Mathematical knowledge management : 5th international conference, MKM 2006, Wokingham, UK, August 11-12, 2006 : proceedings / / Jonathan M. Borwein, William M. Farmer (eds.) |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2006 |
| Descrizione fisica | 1 online resource (VIII, 295 p.) |
| Disciplina | 511.3/6028563 |
| Altri autori (Persone) |
BorweinJonathan M
FarmerWilliam Michael |
| Collana |
Lecture notes in computer science. Lecture notes in artificial intelligence
LNCS sublibrary. SL 7, Artificial intelligence |
| Soggetto topico |
Mathematics - Data processing
Information storage and retrieval systems - Mathematics Automatic theorem proving |
| ISBN | 3-540-37106-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- The Omega Number: Irreducible Complexity in Pure Math -- Roles of Math Search in Mathematics -- Contributed Papers -- Structured Induction Proofs in Isabelle/Isar -- Interpretation of Locales in Isabelle: Theories and Proof Contexts -- A Dynamic Poincaré Principle -- A Proof-Theoretic Approach to Tactics -- A Formal Correspondence Between OMDoc with Alternative Proofs and the -Calculus -- Proof Transformation by CERES -- Synthesizing Proof Planning Methods and ?-Ants Agents from Mathematical Knowledge -- Verifying and Invalidating Textbook Proofs Using Scunak -- Capturing Abstract Matrices from Paper -- Towards a Parser for Mathematical Formula Recognition -- Stochastic Modelling of Scientific Terms Distribution in Publications -- Capturing the Content of Physics: Systems, Observables, and Experiments -- Communities of Practice in MKM: An Extensional Model -- From Notation to Semantics: There and Back Again -- Managing Informal Mathematical Knowledge: Techniques from Informal Logic -- From Untyped to Polymorphically Typed Objects in Mathematical Web Services -- Managing Automatically Formed Mathematical Theories -- Authoring LeActiveMath Calculus Content -- Information Retrieval and Rendering with MML Query -- Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories. |
| Altri titoli varianti | MKM 2006 |
| Record Nr. | UNINA-9910767556503321 |
| Berlin ; ; New York, : Springer, c2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Mathematical knowledge management : 4th international conference, MKM 2005, Bremen, Germany, July 15-17, 2005 : revised selected papers / / Michael Kohlhase (ed.)
| Mathematical knowledge management : 4th international conference, MKM 2005, Bremen, Germany, July 15-17, 2005 : revised selected papers / / Michael Kohlhase (ed.) |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin, : Springer, c2006 |
| Descrizione fisica | 1 online resource (XII, 408 p.) |
| Disciplina | 510.285 |
| Altri autori (Persone) | KohlhaseMichael <1964-> |
| Collana | Lecture notes in computer science,Lecture notes in artificial intelligence |
| Soggetto topico |
Mathematics - Data processing
Information storage and retrieval systems - Mathematics Automatic theorem proving |
| ISBN | 3-540-31431-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Session I: Foundations -- A Proof-Theoretic Approach to Hierarchical Math Library Organization -- An Exploration in the Space of Mathematical Knowledge -- Session II: Authoring -- Authoring Presentation for open math -- Translating Mathematical Vernacular into Knowledge Repositories -- Assisted Proof Document Authoring -- Session III: Representations -- A Tough Nut for Mathematical Knowledge Management -- Textbook Proofs Meet Formal Logic – The Problem of Underspecification and Granularity -- Processing Textbook-Style Matrices -- Session IV: Proving -- A Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity -- Impasse-Driven Reasoning in Proof Planning -- Literate Proving: Presenting and Documenting Formal Proofs -- Session V: MKManagement Tools -- Semantic Matching for Mathematical Services -- Mathematical Knowledge Browser with Automatic Hyperlink Detection -- A Database of Glyphs for OCR of Mathematical Documents -- Session VI: Documents -- Toward an Object-Oriented Structure for Mathematical Text -- Explanation in Natural Language of ?????-Terms -- Engineering Mathematical Knowledge -- Session VII: MKM Case Studies -- Computational Origami of a Morley’s Triangle -- Designing Diagrammatic Catalogues of Types of Basic Interval Equation: A Case Study -- Gröbner Bases — Theory Refinement in the Mizar System -- Session VIII: Course Materials -- An Interactive Algebra Course with Formalised Proofs and Definitions -- Interactive Learning and Mathematical Calculus -- Session IX: Migration -- XML-izing Mizar: Making Semantic Processing and Presentation of MML Easy -- Determining Empirical Characteristics of Mathematical Expression Use -- Transformations of MML Database’s Elements -- Translating a Fragment of Weak Type Theory into Type Theory with Open Terms. |
| Altri titoli varianti | MKM 2005 |
| Record Nr. | UNINA-9910484222903321 |
| Berlin, : Springer, c2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Mathematics mechanization and applications [e-book] / edited by Xiao-Shan Gao and Dongming Wang
| Mathematics mechanization and applications [e-book] / edited by Xiao-Shan Gao and Dongming Wang |
| Pubbl/distr/stampa | San Diego : Academic Press, c2000 |
| Descrizione fisica | xix, 551 p. : ill. ; 26 cm |
| Disciplina | 512.94 |
| Altri autori (Persone) |
Gao, Xiao-Shan
Wang, Dongming |
| Soggetto topico |
Equations - Numerical solutions - Data processing
Automatic theorem proving |
| ISBN |
9780127347608
0127347607 |
| Formato | Risorse elettroniche  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISALENTO-991003278409707536 |
| San Diego : Academic Press, c2000 | ||
| Risorse elettroniche | ||
| Lo trovi qui: Univ. del Salento | ||
| ||
Mechanizing mathematical reasoning : essays in honor of Jorg H. Siekmann on the occasion of his 60th birthday / / Dieter Hutter, Werner Stephan (eds.)
| Mechanizing mathematical reasoning : essays in honor of Jorg H. Siekmann on the occasion of his 60th birthday / / Dieter Hutter, Werner Stephan (eds.) |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, 2005 |
| Descrizione fisica | 1 online resource (X, 570 p.) |
| Disciplina | 511.3/6/028563 |
| Altri autori (Persone) |
SiekmannJorg H
HutterDieter StephanWerner |
| Collana | Lecture notes in computer science,Lecture notes in artificial intelligence |
| Soggetto topico |
Automatic theorem proving
Logic, Symbolic and mathematical Reasoning - Automation Reasoning - Technique |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | A Portrait of a Scientist: Logic, AI and Politics -- A Portrait of a Scientist: Logic, AI and Politics -- Logic and Deduction -- Some Reflections on Proof Transformations -- Rewrite and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation -- SAT-Based Decision Procedures for Automated Reasoning: A Unifying Perspective -- Temporal Dynamics of Support and Attack Networks: From Argumentation to Zoology -- Footprints of Conditionals -- Time for Thinking Big in AI -- Solving First-Order Constraints over the Monadic Class -- From MKRP to ?MEGA -- Decidable Variants of Higher-Order Unification -- Normal Natural Deduction Proofs (in Non-classical Logics) -- History and Future of Implicit and Inductionless Induction: Beware the Old Jade and the Zombie! -- The Flowering of Automated Reasoning -- Applications of Logics -- Description Logics as Ontology Languages for the Semantic Web -- Living Books, Automated Deduction and Other Strange Things -- An Essay on Sabotage and Obstruction -- Bridging Theorem Proving and Mathematical Knowledge Retrieval -- Formal Description of Natural Languages: An HPSG Grammar of Polish -- Psychological Validity of Schematic Proofs -- Natural Language Proof Explanation -- Why Proof Planning for Maths Education and How? -- Formal Methods and Security -- Towards MultiMedia Instruction in Safe and Secure Systems -- The Impact of Models in Software Development -- Formal Software Development in MAYA -- A Unification Algorithm for Analysis of Protocols with Blinded Signatures -- Exploiting Generic Aspects of Security Models in Formal Developments -- Verification Support Environment -- Agents and Planning -- SAT-Based Cooperative Planning: A Proposal -- Towards Comprehensive Computational Models for Plan-Based Control of Autonomous Robots -- Agents with Exact Foreknowledge -- Self-organisation in Holonic Multiagent Systems. |
| Record Nr. | UNINA-9910484271403321 |
| Berlin ; ; New York, : Springer, 2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Proof technology and computation [[electronic resource] /] / edited by Helmut Schwichtenberg and Katharina Spies
| Proof technology and computation [[electronic resource] /] / edited by Helmut Schwichtenberg and Katharina Spies |
| Pubbl/distr/stampa | Amsterdam ; ; Washington, DC, : IOS Press, c2006 |
| Descrizione fisica | 1 online resource (456 p.) |
| Disciplina | 511.3 |
| Altri autori (Persone) |
SchwichtenbergHelmut <1942->
SpiesKatharina |
| Collana | NATO science series. Series III, Computer and systems sciences |
| Soggetto topico |
Automatic theorem proving
Computer programming Computer software - Development |
| Soggetto genere / forma | Electronic books. |
| ISBN |
661054767X
1-280-54767-7 9786610547678 1-4237-9755-8 1-60750-180-5 600-00-0528-8 1-60129-484-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Title page; Preface; Contents; Information-Intensive Proof Technology; Introduction to Proof Theory; The Abstraction-Refinement Framework in Model Checking; Verification: Industrial Applications; Selected Topics on Computability, Complexity, and Termination; Jinja: Towards a Comprehensive Formal Semantics for a Java-like Language; The Formulae-as-Classes Interpretation of Constructive Set Theory; Constructive Analysis with Witnesses; Predicates as Types; Automata- and Logic-Based Systems Design; Recursions and Proofs; Author Index |
| Record Nr. | UNINA-9910450834903321 |
| Amsterdam ; ; Washington, DC, : IOS Press, c2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Proof technology and computation [[electronic resource] /] / edited by Helmut Schwichtenberg and Katharina Spies
| Proof technology and computation [[electronic resource] /] / edited by Helmut Schwichtenberg and Katharina Spies |
| Pubbl/distr/stampa | Amsterdam ; ; Washington, DC, : IOS Press, c2006 |
| Descrizione fisica | 1 online resource (456 p.) |
| Disciplina | 511.3 |
| Altri autori (Persone) |
SchwichtenbergHelmut <1942->
SpiesKatharina |
| Collana | NATO science series. Series III, Computer and systems sciences |
| Soggetto topico |
Automatic theorem proving
Computer programming Computer software - Development |
| ISBN |
661054767X
1-280-54767-7 9786610547678 1-4237-9755-8 1-60750-180-5 600-00-0528-8 1-60129-484-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Title page; Preface; Contents; Information-Intensive Proof Technology; Introduction to Proof Theory; The Abstraction-Refinement Framework in Model Checking; Verification: Industrial Applications; Selected Topics on Computability, Complexity, and Termination; Jinja: Towards a Comprehensive Formal Semantics for a Java-like Language; The Formulae-as-Classes Interpretation of Constructive Set Theory; Constructive Analysis with Witnesses; Predicates as Types; Automata- and Logic-Based Systems Design; Recursions and Proofs; Author Index |
| Record Nr. | UNINA-9910784245903321 |
| Amsterdam ; ; Washington, DC, : IOS Press, c2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
