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.
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 | ||
| ||
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 | ||
| ||
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 | ||
| ||
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 |
| Edizione | [1st ed.] |
| 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-9910827751003321 |
| Amsterdam ; ; Washington, DC, : IOS Press, c2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
