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 : 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010 : revised selected papers / / Edmund M. Clarke, Andrei Voronkov (eds.)
| Logic for Programming, Artificial Intelligence, and Reasoning : 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010 : revised selected papers / / Edmund M. Clarke, Andrei Voronkov (eds.) |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | Berlin, : Springer, 2010 |
| Descrizione fisica | 1 online resource (X, 517 p. 71 illus., 4 illus. in color.) |
| Disciplina | 006.3 |
| Altri autori (Persone) |
ClarkeE. M. <1945->
VoronkovA <1959-> (Andrei) |
| Collana |
Lecture notes in computer science
LNCS sublibrary. SL 7, Artificial intelligence |
| Soggetto topico |
Artificial intelligence
Automatic theorem proving Logic programming |
| ISBN |
1-283-47738-6
9786613477385 3-642-17511-2 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Altri titoli varianti | LPAR-16 |
| Record Nr. | UNINA-9910483030403321 |
| Berlin, : Springer, 2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
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 | ||
| ||
Perspectives of systems informatics : 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009 ; revised papers / / Amir Pnueli, Irina Virbitskaite, Andrei Voronkov (eds.)
| Perspectives of systems informatics : 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009 ; revised papers / / Amir Pnueli, Irina Virbitskaite, Andrei Voronkov (eds.) |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2010 |
| Descrizione fisica | 1 online resource (XIII, 426 p.) |
| Disciplina | 005.1 |
| Altri autori (Persone) |
PnueliA
VirbitskaiteIrina VoronkovA <1959-> (Andrei) |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Computer programming
Computer science Systems engineering |
| ISBN |
1-280-38552-9
9786613563446 3-642-11486-5 |
| Classificazione | SS 4800 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Games, Interaction and Computation -- Rôle of Domain Engineering in Software Development—Why Current Requirements Engineering Is Flawed ! -- Compositional and Quantitative Model Checking (Extended Abstract) -- Invariants, Modularity, and Rights -- Distributed Embedded Systems: Reconciling Computation, Communication and Resource Interaction -- Regular Papers -- Simulation of Kohn’s Molecular Interaction Maps through Translation into Stochastic CLS+ -- A Two-Level Approach for Modeling and Verification of Telecommunication Systems -- SVM Paradoxes -- Indexing Dense Nested Metric Spaces for Efficient Similarity Search -- On the Containment Problem for Queries in Conjunctive Form with Negation -- Towards a Scalable, Pragmatic Knowledge Representation Language for the Web -- An Experiment with the Fourth Futamura Projection -- Extracting the Essence of Distillation -- Establishing Linux Driver Verification Process -- A Method for Test Suite Reduction for Regression Testing of Interactions between Software Modules -- A Java Supercompiler and Its Application to Verification of Cache-Coherence Protocols -- Proving the Equivalence of Higher-Order Terms by Means of Supercompilation -- Unifying the Semantics of UML 2 State, Activity and Interaction Diagrams -- Applicability of the BLAST Model Checker: An Industrial Case Study -- ? K –constraints for Hybrid Systems -- A Complete Invariant Generation Approach for P-solvable Loops -- Standardization and Testing of Mathematical Functions -- Using AOP for Discovering and Defining Executable Test Cases -- Cryptographic Protocols Analysis in Event B -- A Query Language for Logic Architectures -- Planet Map Generation by Tetrahedral Subdivision -- Towards Checking Parametric Reachability for UML State Machines -- A Flexible Approach to Automated Development of Cross Toolkits for Embedded Systems -- A Technique for Information Retrieval from Microformatted Websites -- From Dynamic to Static and Back: Riding the Roller Coaster of Information-Flow Control Research -- History-Dependent Stochastic Petri Nets -- Privacy Preserving Modules for Ontologies -- Symbolic Bounded Conformance Checking of Model Programs -- Multi-level Virtual Machine Debugging Using the Java Platform Debugger Architecture -- Anti-unification Algorithms and Their Applications in Program Analysis. |
| Altri titoli varianti | PSI 2009 |
| Record Nr. | UNINA-9910484946603321 |
| Berlin ; ; New York, : Springer, c2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||