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.
Automated deduction in geometry : Second International Workshop, ADG '98, Beijing, China, August 1998 : proceedings / / Xiao-Shan Gao, Dongming Wang, Lu Yang, editors
| Automated deduction in geometry : Second International Workshop, ADG '98, Beijing, China, August 1998 : proceedings / / Xiao-Shan Gao, Dongming Wang, Lu Yang, editors |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer, , [1999] |
| Descrizione fisica | 1 online resource (VIII, 292 p.) |
| Disciplina | 516.00285 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Geometry - Data processing
Automatic theorem proving |
| ISBN | 3-540-47997-X |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Automatic Geometry Theorem-Proving and Automatic Geometry Problem-Solving -- Solving Geometric Problems with Real Quantifier Elimination -- Automated Discovering and Proving for Geometric Inequalities -- Proving Newton’s Propositio Kepleriana Using Geometry and Nonstandard Analysis in Isabelle -- Readable Machine Solving in Geometry and ICAI Software MSG -- Plane Euclidean Reasoning -- A Clifford Algebraic Method for Geometric Reasoning -- Clifford Term Rewriting for Geometric Reasoning in 3D -- Some Applications of Clifford Algebra to Geometries -- Decomposing Algebraic Varieties -- An Application of Automatic Theorem Proving in Computer Vision -- Automated Geometry Diagram Construction and Engineering Geometry -- A 2D Geometric Constraint Solver for Parametric Design Using Graph Analysis and Reduction -- Variant Geometry Analysis and Synthesis in Mechanical CAD. |
| Record Nr. | UNINA-9910768475903321 |
| Berlin ; ; Heidelberg : , : Springer, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated reasoning : 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings / / editors, Jasmin Blanchette, Laura Kovács, Dirk Pattinson
| Automated reasoning : 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings / / editors, Jasmin Blanchette, Laura Kovács, Dirk Pattinson |
| Autore | Blanchette Jasmin |
| Pubbl/distr/stampa | Cham, : Springer Nature, 2022 |
| Descrizione fisica | 1 online resource (xv, 756 pages) : illustrations (some color) |
| Disciplina | 006.333 |
| Altri autori (Persone) |
BlanchetteJasmin
KovácsLaura PattinsonDirk <1970-> |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Automatic theorem proving
Computer logic |
| Soggetto non controllato |
artificial intelligence
automata theory computer hardware computer networks computer programming computer systems embedded systems formal languages formal logic logic programming network protocols semantics software architecture software design software engineering theoretical computer science |
| ISBN | 3-031-10769-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910585785003321 |
Blanchette Jasmin
|
||
| Cham, : Springer Nature, 2022 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated reasoning : 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings / / editors, Jasmin Blanchette, Laura Kovács, Dirk Pattinson
| Automated reasoning : 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings / / editors, Jasmin Blanchette, Laura Kovács, Dirk Pattinson |
| Autore | Blanchette Jasmin |
| Pubbl/distr/stampa | Cham, : Springer Nature, 2022 |
| Descrizione fisica | 1 online resource (xv, 756 pages) : illustrations (some color) |
| Disciplina | 006.333 |
| Altri autori (Persone) |
BlanchetteJasmin
KovácsLaura PattinsonDirk <1970-> |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Automatic theorem proving
Computer logic |
| Soggetto non controllato |
artificial intelligence
automata theory computer hardware computer networks computer programming computer systems embedded systems formal languages formal logic logic programming network protocols semantics software architecture software design software engineering theoretical computer science |
| ISBN | 3-031-10769-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996483156703316 |
|
Blanchette Jasmin
|
||
| Cham, : Springer Nature, 2022 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated reasoning with analytic tableaux and related methods : 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021 : proceedings / / Anupam Das, Sara Negri, (editors)
| Automated reasoning with analytic tableaux and related methods : 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021 : proceedings / / Anupam Das, Sara Negri, (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (476 pages) |
| Disciplina | 004.015113 |
| Collana | Lecture notes in computer science. Lecture notes in artificial intelligence |
| Soggetto topico | Automatic theorem proving |
| ISBN | 3-030-86059-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910495194603321 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated reasoning with analytic tableaux and related methods : 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021 : proceedings / / Anupam Das, Sara Negri, (editors)
| Automated reasoning with analytic tableaux and related methods : 30th International Conference, TABLEAUX 2021, Birmingham, UK, September 6-9, 2021 : proceedings / / Anupam Das, Sara Negri, (editors) |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2021] |
| Descrizione fisica | 1 online resource (476 pages) |
| Disciplina | 004.015113 |
| Collana | Lecture notes in computer science. Lecture notes in artificial intelligence |
| Soggetto topico | Automatic theorem proving |
| ISBN | 3-030-86059-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996464492203316 |
| Cham, Switzerland : , : Springer, , [2021] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated reasoning with analytic tableaux and related methods : international conference, TABLEAUX 2007, Aix en Provence, France, July 2007, proceedings / / Nicola Olivetti (editor)
| Automated reasoning with analytic tableaux and related methods : international conference, TABLEAUX 2007, Aix en Provence, France, July 2007, proceedings / / Nicola Olivetti (editor) |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer-Verlag, , [2007] |
| Descrizione fisica | 1 online resource (X, 250 p.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico | Automatic theorem proving |
| ISBN | 3-540-73099-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Nonmonotonic Description Logics – Requirements, Theory, and Implementations -- Our Quest for the Holy Grail of Agent Verification -- An Abstract Framework for Satisfiability Modulo Theories -- Research Papers -- Axiom Pinpointing in General Tableaux -- Proof Theory for First Order ?ukasiewicz Logic -- A Tableau Method for Public Announcement Logics -- Bounded Model Checking with Description Logic Reasoning -- Tableau Systems for Logics of Subinterval Structures over Dense Orderings -- A Cut-Free Sequent Calculus for Bi-intuitionistic Logic -- Tableaux with Dynamic Filtration for Layered Modal Logics -- The Neighbourhood of S0.9 and S1 -- EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies -- Tree-Sequent Methods for Subintuitionistic Predicate Logics -- A Sequent Calculus for Bilattice-Based Logic and Its Many-Sorted Representation -- Updating Reduced Implicate Tries -- A Bottom-Up Approach to Clausal Tableaux -- Differential Dynamic Logic for Verifying Parametric Hybrid Systems -- System Descriptions -- Improvements to the Tableau Prover PITP -- KLMLean 2.0: A Theorem Prover for KLM Logics of Nonmonotonic Reasoning. |
| Record Nr. | UNINA-9910485002003321 |
| Berlin, Heidelberg : , : Springer-Verlag, , [2007] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated reasoning with analytic tableaux and related methods : international conference, TABLEAUX 2007, Aix en Provence, France, July 2007, proceedings / / Nicola Olivetti (editor)
| Automated reasoning with analytic tableaux and related methods : international conference, TABLEAUX 2007, Aix en Provence, France, July 2007, proceedings / / Nicola Olivetti (editor) |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer-Verlag, , [2007] |
| Descrizione fisica | 1 online resource (X, 250 p.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico | Automatic theorem proving |
| ISBN | 3-540-73099-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Nonmonotonic Description Logics – Requirements, Theory, and Implementations -- Our Quest for the Holy Grail of Agent Verification -- An Abstract Framework for Satisfiability Modulo Theories -- Research Papers -- Axiom Pinpointing in General Tableaux -- Proof Theory for First Order ?ukasiewicz Logic -- A Tableau Method for Public Announcement Logics -- Bounded Model Checking with Description Logic Reasoning -- Tableau Systems for Logics of Subinterval Structures over Dense Orderings -- A Cut-Free Sequent Calculus for Bi-intuitionistic Logic -- Tableaux with Dynamic Filtration for Layered Modal Logics -- The Neighbourhood of S0.9 and S1 -- EXPTIME Tableaux with Global Caching for Description Logics with Transitive Roles, Inverse Roles and Role Hierarchies -- Tree-Sequent Methods for Subintuitionistic Predicate Logics -- A Sequent Calculus for Bilattice-Based Logic and Its Many-Sorted Representation -- Updating Reduced Implicate Tries -- A Bottom-Up Approach to Clausal Tableaux -- Differential Dynamic Logic for Verifying Parametric Hybrid Systems -- System Descriptions -- Improvements to the Tableau Prover PITP -- KLMLean 2.0: A Theorem Prover for KLM Logics of Nonmonotonic Reasoning. |
| Record Nr. | UNISA-996465913103316 |
| Berlin, Heidelberg : , : Springer-Verlag, , [2007] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated reasoning with analytic tableaux and related methods : international conference, TABLEAUX'99, Saratoga Springs, NY, June 7-11, 1999 : proceedings / / Neil V. Murray, editor
| Automated reasoning with analytic tableaux and related methods : international conference, TABLEAUX'99, Saratoga Springs, NY, June 7-11, 1999 : proceedings / / Neil V. Murray, editor |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer Verlag, , [1999] |
| Descrizione fisica | 1 online resource (X, 334 p.) |
| Disciplina | 511.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico | Automatic theorem proving |
| ISBN | 3-540-48754-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Extended Abstracts of Invited Lectures -- Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions -- Comparison -- Design and Results of the Tableaux-99 Non-classical (Modal) Systems Comparison -- DLP and FaCT -- Applying an ABox Consistency Tester to Modal Logic SAT Problems -- KtSeqC : System Description -- Abstracts of Tutorials -- Automated Reasoning and the Verification of Security Protocols -- Proof Confluent Tableau Calculi -- Contributed Research Papers -- Analytic Calculi for Projective Logics -- Merge Path Improvements for Minimal Model Hyper Tableaux -- CLDS for Propositional Intuitionistic Logic -- Intuitionisitic Tableau Extracted -- A Tableau-Based Decision Procedure for a Fragment of Set Theory Involving a Restricted Form of Quantification -- Bounded Contraction in Systems with Linearity -- The Non-associative Lambek Calculus with Product in Polynomial Time -- Sequent Calculi for Nominal Tense Logics: A Step Towards Mechanization? -- Cut-Free Display Calculi for Nominal Tense Logics -- Hilbert’s ?-Terms in Automated Theorem Proving -- Partial Functions in an Impredicative Simple Theory of Types -- A Simple Sequent System for First-Order Logic with Free Constructors -- linTAP : A Tableau Prover for Linear Logic -- A Tableau Calculus for a Temporal Logic with Temporal Connectives -- A Tableau Calculus for Pronoun Resolution -- Generating Minimal Herbrand Models Step by Step -- Tableau Calculi for Hybrid Logics -- Full First-Order Free Variable Sequents and Tableaux in Implicit Induction -- Contributed System Descriptions -- An Interactive Theorem Proving Assistant -- A Time Efficient KE Based Theorem Prover -- Strategy Parallel Use of Model Elimination with Lemmata. |
| Record Nr. | UNINA-9910143644403321 |
| Berlin ; ; Heidelberg : , : Springer Verlag, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated reasoning with analytic tableaux and related methods : international conference, TABLEAUX'99, Saratoga Springs, NY, June 7-11, 1999 : proceedings / / Neil V. Murray, editor
| Automated reasoning with analytic tableaux and related methods : international conference, TABLEAUX'99, Saratoga Springs, NY, June 7-11, 1999 : proceedings / / Neil V. Murray, editor |
| Edizione | [1st ed. 1999.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer Verlag, , [1999] |
| Descrizione fisica | 1 online resource (X, 334 p.) |
| Disciplina | 511.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico | Automatic theorem proving |
| ISBN | 3-540-48754-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Extended Abstracts of Invited Lectures -- Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions -- Comparison -- Design and Results of the Tableaux-99 Non-classical (Modal) Systems Comparison -- DLP and FaCT -- Applying an ABox Consistency Tester to Modal Logic SAT Problems -- KtSeqC : System Description -- Abstracts of Tutorials -- Automated Reasoning and the Verification of Security Protocols -- Proof Confluent Tableau Calculi -- Contributed Research Papers -- Analytic Calculi for Projective Logics -- Merge Path Improvements for Minimal Model Hyper Tableaux -- CLDS for Propositional Intuitionistic Logic -- Intuitionisitic Tableau Extracted -- A Tableau-Based Decision Procedure for a Fragment of Set Theory Involving a Restricted Form of Quantification -- Bounded Contraction in Systems with Linearity -- The Non-associative Lambek Calculus with Product in Polynomial Time -- Sequent Calculi for Nominal Tense Logics: A Step Towards Mechanization? -- Cut-Free Display Calculi for Nominal Tense Logics -- Hilbert’s ?-Terms in Automated Theorem Proving -- Partial Functions in an Impredicative Simple Theory of Types -- A Simple Sequent System for First-Order Logic with Free Constructors -- linTAP : A Tableau Prover for Linear Logic -- A Tableau Calculus for a Temporal Logic with Temporal Connectives -- A Tableau Calculus for Pronoun Resolution -- Generating Minimal Herbrand Models Step by Step -- Tableau Calculi for Hybrid Logics -- Full First-Order Free Variable Sequents and Tableaux in Implicit Induction -- Contributed System Descriptions -- An Interactive Theorem Proving Assistant -- A Time Efficient KE Based Theorem Prover -- Strategy Parallel Use of Model Elimination with Lemmata. |
| Record Nr. | UNISA-996465333503316 |
| Berlin ; ; Heidelberg : , : Springer Verlag, , [1999] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated reasoning with analytic tableaux and related methods : International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, May 5-8, 1998 : proceedings / / Harrie de Swart (editor)
| Automated reasoning with analytic tableaux and related methods : International Conference, TABLEAUX'98, Oisterwijk, The Netherlands, May 5-8, 1998 : proceedings / / Harrie de Swart (editor) |
| Edizione | [1st ed. 1998.] |
| Pubbl/distr/stampa | Berlin : , : Springer, , [1998] |
| Descrizione fisica | 1 online resource (X, 325 p.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Automatic theorem proving
Artificial intelligence |
| ISBN | 3-540-69778-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Extended Abstracts of Invited Lectures -- Philosophical Aspects of Computerized Verification of Mathematics -- A Science of Reasoning (Extended Abstract) -- Model Checking: Historical Perspective and Example (Extended Abstract) -- Comparison -- Comparison of Theorem Provers for Modal Logics — Introduction and Summary -- FaCT and DLP -- Prover KT4 -- leanK 2.0 -- Logics Workbench 1.0 -- Optimised Functional Translation and Resolution -- Benchmark Evaluation of ?KE -- Abstracts of the Tutorials -- Implementation of Propositional Temporal Logics Using BDDs -- Computer Programming as Mathematics in a Programming Language and Proof System CL -- Contributed Research Papers -- A Tableau Calculus for Multimodal Logics and Some (Un)Decidability Results -- Hyper Tableau — The Next Generation -- Fibring Semantic Tableaux -- A Tableau Calculus for Quantifier-Free Set Theoretic Formulae -- A Tableau Method for Interval Temporal Logic with Projection -- Bounded Model Search in Linear Temporal Logic and Its Application to Planning -- On Proof Complexity of Circumscription -- Tableaux for Finite-Valued Logics with Arbitrary Distribution Modalities -- Some Remarks on Completeness, Connection Graph Resolution, and Link Deletion -- Simplification and Backjumping in Modal Tableau -- Free Variable Tableaux for a Logic with Term Declarations -- Simplification A General Constraint Propagation Technique for Propositional and Modal Tableaux -- A Tableaux Calculus for Ambiguous Quantifiation -- From Kripke Models to Algebraic Counter-Valuations -- Deleting Redundancy in Proof Reconstruction -- A New One-Pass Tableau Calculus for PLTL -- Decision Procedures for Intuitionistic Propositional Logic by Program Extraction -- Contributed System Descriptions -- The FaCT System -- Implementation of Proof Search in the Imperative Programming Language Pizza -- p-SETHEO: Strategy Parallelism in Automated Theorem Proving. |
| Record Nr. | UNINA-9910143452803321 |
| Berlin : , : Springer, , [1998] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
