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.
Formal Methods in Computer-Aided Design
| Formal Methods in Computer-Aided Design |
| Pubbl/distr/stampa | Los Alamitos, California : , : IEEE Computer Society |
| Descrizione fisica | online resource |
| Disciplina | 621.3815 |
| Soggetto topico |
Digital integrated circuits - Computer-aided design
Digital integrated circuits - Design and construction - Data processing Computer-aided design Automatic theorem proving Integrated circuits - Verification |
| Soggetto genere / forma |
Periodicals.
Conference papers and proceedings. |
| ISSN | 2642-732X |
| Formato | Materiale a stampa  |
| Livello bibliografico | Periodico |
| Lingua di pubblicazione | eng |
| Altri titoli varianti |
Proceedings of
Proceedings of Formal Methods in Computer-Aided Design FMCAD .. |
| Record Nr. | UNINA-9910626187403321 |
| Los Alamitos, California : , : IEEE Computer Society | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Interactive theorem proving : 1st International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010 : proceedings / / Matt Kaufmann, Lawrence C. Paulson, (eds.)
| Interactive theorem proving : 1st International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010 : proceedings / / Matt Kaufmann, Lawrence C. Paulson, (eds.) |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | Berlin, : Springer, 2010 |
| Descrizione fisica | 1 online resource (XI, 495 p. 82 illus.) |
| Disciplina | 005.1015113 |
| Altri autori (Persone) |
KaufmannMatt
PaulsonLawrence C |
| Collana |
Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
| Soggetto topico | Automatic theorem proving |
| ISBN |
1-280-38759-9
9786613565518 3-642-14052-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- A Formally Verified OS Kernel. Now What? -- Proof Assistants as Teaching Assistants: A View from the Trenches -- Proof Pearls -- A Certified Denotational Abstract Interpreter -- Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure -- A New Foundation for Nominal Isabelle -- (Nominal) Unification by Recursive Descent with Triangular Substitutions -- A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks -- Regular Papers -- Extending Coq with Imperative Features and Its Application to SAT Verification -- A Tactic Language for Declarative Proofs -- Programming Language Techniques for Cryptographic Proofs -- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder -- Formal Proof of a Wave Equation Resolution Scheme: The Method Error -- An Efficient Coq Tactic for Deciding Kleene Algebras -- Fast LCF-Style Proof Reconstruction for Z3 -- The Optimal Fixed Point Combinator -- Formal Study of Plane Delaunay Triangulation -- Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison -- A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture -- Automated Machine-Checked Hybrid System Safety Proofs -- Coverset Induction with Partiality and Subsorts: A Powerlist Case Study -- Case-Analysis for Rippling and Inductive Proof -- Importing HOL Light into Coq -- A Mechanized Translation from Higher-Order Logic to Set Theory -- The Isabelle Collections Framework -- Interactive Termination Proofs Using Termination Cores -- A Framework for Formal Verification of Compiler Optimizations -- On the Formalization of the Lebesgue Integration Theory in HOL -- From Total Store Order to Sequential Consistency: A Practical Reduction Theorem -- Equations: A Dependent Pattern-Matching Compiler -- A Mechanically Verified AIG-to-BDD Conversion Algorithm -- Inductive Consequences in the Calculus of Constructions -- Validating QBF Invalidity in HOL4 -- Rough Diamonds -- Higher-Order Abstract Syntax in Isabelle/HOL -- Separation Logic Adapted for Proofs by Rewriting -- Developing the Algebraic Hierarchy with Type Classes in Coq. |
| Record Nr. | UNINA-9910483708703321 |
| Berlin, : Springer, 2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Journal of automated reasoning
| Journal of automated reasoning |
| Pubbl/distr/stampa | [Dordrecht], : Kluwer Academic Publishers |
| Disciplina | 511.3 |
| Soggetto topico |
Automatic theorem proving
Artificial intelligence Logic programming Théorèmes - Démonstration automatique Intelligence artificielle Programmation logique |
| ISSN | 1573-0670 |
| Formato | Materiale a stampa |
| Livello bibliografico | Periodico |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996207918603316 |
| [Dordrecht], : Kluwer Academic Publishers | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Journal of automated reasoning
| Journal of automated reasoning |
| Pubbl/distr/stampa | [Dordrecht], : Kluwer Academic Publishers |
| Disciplina | 511.3 |
| Soggetto topico |
Automatic theorem proving
Artificial intelligence Logic programming Théorèmes - Démonstration automatique Intelligence artificielle Programmation logique |
| ISSN | 1573-0670 |
| Formato | Materiale a stampa |
| Livello bibliografico | Periodico |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910142430903321 |
| [Dordrecht], : Kluwer Academic Publishers | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
The little prover / / Daniel P. Friedman, Carl Eastlund ; drawings by Duane Bibby ; foreword by J Strother More
| The little prover / / Daniel P. Friedman, Carl Eastlund ; drawings by Duane Bibby ; foreword by J Strother More |
| Autore | Friedman Daniel P. |
| Pubbl/distr/stampa | Cambridge, Massachusetts : , : MIT Press, , [2015] |
| Descrizione fisica | 1 online resource (244 p.) |
| Disciplina | 511.3/6028563 |
| Altri autori (Persone) | EastlundCarl |
| Soggetto topico |
Automatic theorem proving
LISP (Computer program language) |
| ISBN |
0-262-33057-1
0-262-33056-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Intro; Contents; Foreword; Preface; 1. Old Games, New Rules; 2. Even Older Games; 3. What's in a Name?; 4. Part of This Total Breakfast; 5. Think It Over and Over and Over; 6. Think It Through; 7. Oh My, Stars!; 8. Learning the Rules; 9. Changing the Rules; 10. The Stars Are Aligned; Recess; The Proof of the Pudding; The Little Assistant; Restless for More?; Afterword; Index |
| Record Nr. | UNINA-9910797359703321 |
Friedman Daniel P.
|
||
| Cambridge, Massachusetts : , : MIT Press, , [2015] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
The little prover / / Daniel P. Friedman, Carl Eastlund ; drawings by Duane Bibby ; foreword by J Strother More
| The little prover / / Daniel P. Friedman, Carl Eastlund ; drawings by Duane Bibby ; foreword by J Strother More |
| Autore | Friedman Daniel P. |
| Pubbl/distr/stampa | Cambridge, Massachusetts : , : MIT Press, , [2015] |
| Descrizione fisica | 1 online resource (244 p.) |
| Disciplina | 511.3/6028563 |
| Altri autori (Persone) | EastlundCarl |
| Soggetto topico |
Automatic theorem proving
LISP (Computer program language) |
| ISBN |
0-262-33057-1
0-262-33056-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Intro; Contents; Foreword; Preface; 1. Old Games, New Rules; 2. Even Older Games; 3. What's in a Name?; 4. Part of This Total Breakfast; 5. Think It Over and Over and Over; 6. Think It Through; 7. Oh My, Stars!; 8. Learning the Rules; 9. Changing the Rules; 10. The Stars Are Aligned; Recess; The Proof of the Pudding; The Little Assistant; Restless for More?; Afterword; Index |
| Record Nr. | UNINA-9910825540903321 |
|
Friedman Daniel P.
|
||
| Cambridge, Massachusetts : , : MIT Press, , [2015] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Logic for programming and automated reasoning : 6th international conference, lpar'99, tbilisi, georgia, september 6-10, 1999 : proceedings / / edited by Harald Ganzinger, David McAllester, Andrei Voronkov
| Logic for programming and automated reasoning : 6th international conference, lpar'99, tbilisi, georgia, september 6-10, 1999 : proceedings / / edited by Harald Ganzinger, David McAllester, Andrei Voronkov |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin, Germany : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (409 p.) |
| Disciplina | 005.115 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Automatic theorem proving
Logic programming |
| ISBN |
1-280-95181-8
9786610951819 3-540-48242-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Session 1 -- Proofs About Lists Using Ellipsis -- Session 2 -- On the Complexity of Counting the Hilbert Basis of a Linear Diophantine System -- Solving Combinatorial Problems with Regular Local Search Algorithms -- Evidence Algorithm and Sequent Logical Inference Search -- Session 3 -- First Order Linear Temporal Logic over Finite Time Structures -- Model Checking Games for the Alternation-Free ?-Calculus and Alternating Automata -- Animating TLA Specifications -- Session 4 -- Transforming Conditional Rewrite Systems with Extra Variables into Unconditional Systems -- Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups -- Regular Sets of Descendants for Constructor-Based Rewrite Systems -- Session 5 -- Practical Reasoning for Expressive Description Logics -- Complexity of Terminological Reasoning Revisited -- Session 6 -- On the Complexity of Single-Rule Datalog Queries -- Session 7 -- Abstracting Properties in Concurrent Constraint Programming -- A Fixpoint Semantics for Reasoning about Finite Failure -- Extensions to the Estimation Calculus -- Session 8 -- Beth Definability for the Guarded Fragment -- Simplification of Horn Clauses That Are Clausal Forms of Guarded Formulas -- Session 9 -- Resource Management in Linear Logic Proof Search Revisited -- Focusing and Proof-Nets in Linear and Non-commutative Logic -- Session 10 -- CHAT Is ? (SLG-WAM) -- Proving Failure of Queries for Definite Logic Programs Using XSB-Prolog -- A Partial Evaluation Framework for Curry Programs. |
| Record Nr. | UNISA-996465812503316 |
| Berlin, Germany : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Logic for programming and automated reasoning : 6th international conference, lpar'99, tbilisi, georgia, september 6-10, 1999 : proceedings / / edited by Harald Ganzinger, David McAllester, Andrei Voronkov
| Logic for programming and automated reasoning : 6th international conference, lpar'99, tbilisi, georgia, september 6-10, 1999 : proceedings / / edited by Harald Ganzinger, David McAllester, Andrei Voronkov |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin, Germany : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (409 p.) |
| Disciplina | 005.115 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Automatic theorem proving
Logic programming |
| ISBN |
1-280-95181-8
9786610951819 3-540-48242-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Session 1 -- Proofs About Lists Using Ellipsis -- Session 2 -- On the Complexity of Counting the Hilbert Basis of a Linear Diophantine System -- Solving Combinatorial Problems with Regular Local Search Algorithms -- Evidence Algorithm and Sequent Logical Inference Search -- Session 3 -- First Order Linear Temporal Logic over Finite Time Structures -- Model Checking Games for the Alternation-Free ?-Calculus and Alternating Automata -- Animating TLA Specifications -- Session 4 -- Transforming Conditional Rewrite Systems with Extra Variables into Unconditional Systems -- Cancellative Superposition Decides the Theory of Divisible Torsion-Free Abelian Groups -- Regular Sets of Descendants for Constructor-Based Rewrite Systems -- Session 5 -- Practical Reasoning for Expressive Description Logics -- Complexity of Terminological Reasoning Revisited -- Session 6 -- On the Complexity of Single-Rule Datalog Queries -- Session 7 -- Abstracting Properties in Concurrent Constraint Programming -- A Fixpoint Semantics for Reasoning about Finite Failure -- Extensions to the Estimation Calculus -- Session 8 -- Beth Definability for the Guarded Fragment -- Simplification of Horn Clauses That Are Clausal Forms of Guarded Formulas -- Session 9 -- Resource Management in Linear Logic Proof Search Revisited -- Focusing and Proof-Nets in Linear and Non-commutative Logic -- Session 10 -- CHAT Is ? (SLG-WAM) -- Proving Failure of Queries for Definite Logic Programs Using XSB-Prolog -- A Partial Evaluation Framework for Curry Programs. |
| Record Nr. | UNINA-9910767557003321 |
| Berlin, Germany : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Logic for programming, artificial intelligence, and reasoning : 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010 : proceedings / / Christian G. Fermuller, Andrei Voronkov (eds.)
| Logic for programming, artificial intelligence, and reasoning : 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010 : proceedings / / Christian G. Fermuller, Andrei Voronkov (eds.) |
| Edizione | [1st ed. 2010.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, 2010 |
| Descrizione fisica | 1 online resource (XII, 656 p. 83 illus.) |
| Disciplina | 006.3 |
| Altri autori (Persone) |
FermullerChristian G
VoronkovAndrei |
| Collana |
Lecture notes in computer science
LNCS sublibrary : SL 1. Theoretical computer science and general issues |
| Soggetto topico |
Logic programming
Artificial intelligence Automatic theorem proving |
| ISBN |
1-280-38966-4
9786613567581 3-642-16242-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | The Complexity of Partial-Observation Parity Games -- Awareness in Games, Awareness in Logic -- Human and Unhuman Commonsense Reasoning -- Gödel Logics – A Survey -- Tableau Calculus for the Logic of Comparative Similarity over Arbitrary Distance Spaces -- Extended Computation Tree Logic -- Using Causal Relationships to Deal with the Ramification Problem in Action Formalisms Based on Description Logics -- SAT Encoding of Unification in -- Generating Combinatorial Test Cases by Efficient SAT Encodings Suitable for CDCL SAT Solvers -- Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models -- Characterising Space Complexity Classes via Knuth-Bendix Orders -- Focused Natural Deduction -- How to Universally Close the Existential Rule -- On the Complexity of the Bernays-Schönfinkel Class with Datalog -- Magically Constraining the Inverse Method Using Dynamic Polarity Assignment -- Lazy Abstraction for Size-Change Termination -- A Syntactical Approach to Qualitative Constraint Networks Merging -- On the Satisfiability of Two-Variable Logic over Data Words -- Generic Methods for Formalising Sequent Calculi Applied to Provability Logic -- Characterising Probabilistic Processes Logically -- fCube: An Efficient Prover for Intuitionistic Propositional Logic -- Superposition-Based Analysis of First-Order Probabilistic Timed Automata -- A Nonmonotonic Extension of KLM Preferential Logic P -- On Strong Normalization of the Calculus of Constructions with Type-Based Termination -- Aligators for Arrays (Tool Paper) -- Clause Elimination Procedures for CNF Formulas -- Partitioning SAT Instances for Distributed Solving -- Infinite Families of Finite String Rewriting Systems and Their Confluence -- Polite Theories Revisited -- Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference -- The Consistency of the CADIAG-2 Knowledge Base: A Probabilistic Approach -- On the Complexity of Model Expansion -- Labelled Unit Superposition Calculi for Instantiation-Based Reasoning -- Boosting Local Search Thanks to cdcl -- Interpolating Quantifier-Free Presburger Arithmetic -- Variable Compression in ProbLog -- Improving Resource-Unaware SAT Solvers -- Expansion Nets: Proof-Nets for Propositional Classical Logic -- Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting -- An Isabelle-Like Procedural Mode for HOL Light -- Bottom-Up Tree Automata with Term Constraints -- Constructors, Sufficient Completeness, and Deadlock Freedom of Rewrite Theories -- PBINT, A Logic for Modelling Search Problems Involving Arithmetic -- Resolution for Stochastic Boolean Satisfiability -- Symbolic Automata Constraint Solving. |
| Record Nr. | UNINA-9910483742303321 |
| Berlin ; ; New York, : Springer, 2010 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
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 | ||
| ||
