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 Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings / / edited by Revantha Ramanayake, Josef Urban
| Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings / / edited by Revantha Ramanayake, Josef Urban |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (XXV, 482 p. 370 illus., 12 illus. in color.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Machine theory Computer science Software engineering Computer systems Microprogramming Artificial Intelligence Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Software Engineering Computer System Implementation Control Structures and Microprogramming |
| ISBN | 3-031-43513-3 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Range-Restricted and Horn Interpolation through Clausal Tableaux -- Non-Classical Logics in Satisfiability Modulo Theories -- DefTab: A Tableaux System for Sceptical Consequence in Default Modal Logics -- Non-distributive description logic -- A new calculus for intuitionistic Strong L\"ob logic: strong termination and cut-elimination, formalized -- Some Analytic Systems of Rules -- A cut-free, sound and complete Russellian theory of definite descriptions -- Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators -- Lemmas: Generation, Selection, Application -- Machine-Learned Premise Selection for Lean -- gym-saturation: Gymnasium environments for saturation provers (System description) -- A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points -- Ill-founded Proof Systems For Intuitionistic Linear-time Temporal Logic -- Proof Systems for the Modal $\mu$-Calculus Obtained by Determinizing Automata -- Extensions of K5: Proof Theory and Uniform Lyndon Interpolation -- On intuitionistic diamonds (and lack thereof) -- NP Complexity for Combinations of Non-Normal Modal Logics -- Resolution-based Calculi for Non-Normal Modal Logics -- Canonicity of Proofs in Constructive Modal Logic -- Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic -- The MaxSAT problem in the real-valued MV-algebra -- The Logic of Separation Logic: Models and Proofs -- Testing the Satisfiability of Formulas in Separation Logic with Permissions -- Nested Sequents for Quantified Modal Logics -- A Naive Prover for First-Order Logic: A Minimal Example of Analytic Completeness. |
| Record Nr. | UNISA-996550548203316 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings / / edited by Revantha Ramanayake, Josef Urban
| Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18–21, 2023, Proceedings / / edited by Revantha Ramanayake, Josef Urban |
| Edizione | [1st ed. 2023.] |
| Pubbl/distr/stampa | Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 |
| Descrizione fisica | 1 online resource (XXV, 482 p. 370 illus., 12 illus. in color.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Machine theory Computer science Software engineering Computer systems Microprogramming Artificial Intelligence Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Software Engineering Computer System Implementation Control Structures and Microprogramming |
| ISBN | 3-031-43513-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Range-Restricted and Horn Interpolation through Clausal Tableaux -- Non-Classical Logics in Satisfiability Modulo Theories -- DefTab: A Tableaux System for Sceptical Consequence in Default Modal Logics -- Non-distributive description logic -- A new calculus for intuitionistic Strong L\"ob logic: strong termination and cut-elimination, formalized -- Some Analytic Systems of Rules -- A cut-free, sound and complete Russellian theory of definite descriptions -- Towards Proof-Theoretic Formulation of the General Theory of Term-Forming Operators -- Lemmas: Generation, Selection, Application -- Machine-Learned Premise Selection for Lean -- gym-saturation: Gymnasium environments for saturation provers (System description) -- A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed points -- Ill-founded Proof Systems For Intuitionistic Linear-time Temporal Logic -- Proof Systems for the Modal $\mu$-Calculus Obtained by Determinizing Automata -- Extensions of K5: Proof Theory and Uniform Lyndon Interpolation -- On intuitionistic diamonds (and lack thereof) -- NP Complexity for Combinations of Non-Normal Modal Logics -- Resolution-based Calculi for Non-Normal Modal Logics -- Canonicity of Proofs in Constructive Modal Logic -- Proof-theoretic Semantics for Intuitionistic Multiplicative Linear Logic -- The MaxSAT problem in the real-valued MV-algebra -- The Logic of Separation Logic: Models and Proofs -- Testing the Satisfiability of Formulas in Separation Logic with Permissions -- Nested Sequents for Quantified Modal Logics -- A Naive Prover for First-Order Logic: A Minimal Example of Analytic Completeness. |
| Record Nr. | UNINA-9910744502303321 |
| Cham : , : Springer Nature Switzerland : , : Imprint : Springer, , 2023 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Intelligent Computer Mathematics [[electronic resource] ] : CICM 2014 Joint Events: Calculemus, DML, MKM, and Systems and Projects 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings / / edited by Stephen M. Watt, Alan Sexton, James H. Davenport, Petr Sojka, Josef Urban
| Intelligent Computer Mathematics [[electronic resource] ] : CICM 2014 Joint Events: Calculemus, DML, MKM, and Systems and Projects 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings / / edited by Stephen M. Watt, Alan Sexton, James H. Davenport, Petr Sojka, Josef Urban |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XX, 458 p. 111 illus.) |
| Disciplina | 512 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Computer science—Mathematics
Artificial intelligence Mathematical logic Natural language processing (Computer science) Information storage and retrieval Symbolic and Algebraic Manipulation Artificial Intelligence Math Applications in Computer Science Mathematical Logic and Formal Languages Natural Language Processing (NLP) Information Storage and Retrieval |
| ISBN | 3-319-08434-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks.-What International Studies Say about the Importance and Limitations of Using Computers to Teach Mathematics in Secondary Schools -- Towards Robust Hyperlinks for Web-Based Scholarly Communication -- Computable Data, Mathematics, and Digital Libraries in Mathematica and Wolfram Alpha -- Calculemus -- Towards the Formal Reliability Analysis of Oil and Gas Pipelines -- Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition -- A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata -- Detecting Unknots via Equational Reasoning, I: Exploration -- Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition -- Hipster: Integrating Theory Exploration in a Proof Assistant -- Formalization of Complex Vectors in Higher-Order Logic -- A Mathematical Structure for Modeling Inventions -- Digital Mathematics Library -- Search Interfaces for Mathematicians -- A Data Model and Encoding for a Semantic, Multilingual Terminology of Mathematics -- PDF/A-3u as an Archival Format for Accessible Mathematics -- Which One Is Better: Presentation-Based or Content-Based Math Search? -- POS Tagging and Its Applications for Mathematics -- Mathoid: Robust, Scalable, Fast and Accessible Math Rendering for Wikipedia -- Mathematical Knowledge Management -- Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle? -- Realms: A Structure for Consolidating Knowledge about Mathematical Theories -- Matching Concepts across HOL Libraries -- Mining State-Based Models from Proof Corpora -- Querying Geometric Figures Using a Controlled Language, Ontological Graphs and Dependency Lattices -- Flexary Operators for Formalized Mathematics -- Interactive Simplifier Tracing and Debugging in Isabelle -- Towards an Interaction-based Integration of MKM Services into End-User Applications -- Towards Knowledge Management for HOL Light -- Automated Improving of Proof Legibility in the Mizar System -- A Vernacular for Coherent Logic -- An Approach to Math-Similarity Search -- Systems and Projects -- Digital Repository of Mathematical Formulae -- NNexus Reloaded -- E-books and Graphics with LATExml -- System Description: MathHub.info -- Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description -- System Description: A Semantics-Aware LATEX-to-Office Converter -- Math Indexer and Searcher Web Interface: Towards Fulfillment of Mathematicians’ Information Needs -- SAT-Enhanced Mizar Proof Checking -- A Framework for Formal Reasoning about Geometrical Optics. |
| Record Nr. | UNISA-996199993903316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Intelligent Computer Mathematics : CICM 2014 Joint Events: Calculemus, DML, MKM, and Systems and Projects 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings / / edited by Stephen M. Watt, Alan Sexton, James H. Davenport, Petr Sojka, Josef Urban
| Intelligent Computer Mathematics : CICM 2014 Joint Events: Calculemus, DML, MKM, and Systems and Projects 2014, Coimbra, Portugal, July 7-11, 2014. Proceedings / / edited by Stephen M. Watt, Alan Sexton, James H. Davenport, Petr Sojka, Josef Urban |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XX, 458 p. 111 illus.) |
| Disciplina | 512 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Computer science—Mathematics
Artificial intelligence Mathematical logic Natural language processing (Computer science) Information storage and retrieval Symbolic and Algebraic Manipulation Artificial Intelligence Math Applications in Computer Science Mathematical Logic and Formal Languages Natural Language Processing (NLP) Information Storage and Retrieval |
| ISBN | 3-319-08434-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks.-What International Studies Say about the Importance and Limitations of Using Computers to Teach Mathematics in Secondary Schools -- Towards Robust Hyperlinks for Web-Based Scholarly Communication -- Computable Data, Mathematics, and Digital Libraries in Mathematica and Wolfram Alpha -- Calculemus -- Towards the Formal Reliability Analysis of Oil and Gas Pipelines -- Problem Formulation for Truth-Table Invariant Cylindrical Algebraic Decomposition by Incremental Triangular Decomposition -- A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata -- Detecting Unknots via Equational Reasoning, I: Exploration -- Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition -- Hipster: Integrating Theory Exploration in a Proof Assistant -- Formalization of Complex Vectors in Higher-Order Logic -- A Mathematical Structure for Modeling Inventions -- Digital Mathematics Library -- Search Interfaces for Mathematicians -- A Data Model and Encoding for a Semantic, Multilingual Terminology of Mathematics -- PDF/A-3u as an Archival Format for Accessible Mathematics -- Which One Is Better: Presentation-Based or Content-Based Math Search? -- POS Tagging and Its Applications for Mathematics -- Mathoid: Robust, Scalable, Fast and Accessible Math Rendering for Wikipedia -- Mathematical Knowledge Management -- Set Theory or Higher Order Logic to Represent Auction Concepts in Isabelle? -- Realms: A Structure for Consolidating Knowledge about Mathematical Theories -- Matching Concepts across HOL Libraries -- Mining State-Based Models from Proof Corpora -- Querying Geometric Figures Using a Controlled Language, Ontological Graphs and Dependency Lattices -- Flexary Operators for Formalized Mathematics -- Interactive Simplifier Tracing and Debugging in Isabelle -- Towards an Interaction-based Integration of MKM Services into End-User Applications -- Towards Knowledge Management for HOL Light -- Automated Improving of Proof Legibility in the Mizar System -- A Vernacular for Coherent Logic -- An Approach to Math-Similarity Search -- Systems and Projects -- Digital Repository of Mathematical Formulae -- NNexus Reloaded -- E-books and Graphics with LATExml -- System Description: MathHub.info -- Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description -- System Description: A Semantics-Aware LATEX-to-Office Converter -- Math Indexer and Searcher Web Interface: Towards Fulfillment of Mathematicians’ Information Needs -- SAT-Enhanced Mizar Proof Checking -- A Framework for Formal Reasoning about Geometrical Optics. |
| Record Nr. | UNINA-9910484944603321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Intelligent Computer Mathematics [[electronic resource] ] : 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011, Proceedings / / edited by James H. Davenport, William M. Farmer, Florian Rabe, Josef Urban
| Intelligent Computer Mathematics [[electronic resource] ] : 18th Symposium, Calculemus 2011, and 10th International Conference, MKM 2011, Bertinoro, Italy, July 18-23, 2011, Proceedings / / edited by James H. Davenport, William M. Farmer, Florian Rabe, Josef Urban |
| Edizione | [1st ed. 2011.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 |
| Descrizione fisica | 1 online resource (XIII, 312 p.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Application software Database management Information storage and retrieval Mathematical logic Data mining Artificial Intelligence Information Systems Applications (incl. Internet) Database Management Information Storage and Retrieval Mathematical Logic and Formal Languages Data Mining and Knowledge Discovery |
| ISBN | 3-642-22673-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996465968403316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Mathematical Software – ICMS 2018 [[electronic resource] ] : 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings / / edited by James H. Davenport, Manuel Kauers, George Labahn, Josef Urban
| Mathematical Software – ICMS 2018 [[electronic resource] ] : 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings / / edited by James H. Davenport, Manuel Kauers, George Labahn, Josef Urban |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XIX, 508 p. 132 illus.) |
| Disciplina | 510.285 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science—Mathematics
Discrete mathematics Artificial intelligence Data protection Computer programming Compilers (Computer programs) Information storage and retrieval systems Discrete Mathematics in Computer Science Artificial Intelligence Data and Information Security Programming Techniques Compilers and Interpreters Information Storage and Retrieval |
| ISBN | 3-319-96418-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Logic -- Number theory -- Combinatorics -- Algebra -- Analysis -- Geometry -- Inter-disciplinary -- Mathematical problem solving platform. |
| Record Nr. | UNISA-996466184003316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Mathematical Software – ICMS 2018 : 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings / / edited by James H. Davenport, Manuel Kauers, George Labahn, Josef Urban
| Mathematical Software – ICMS 2018 : 6th International Conference, South Bend, IN, USA, July 24-27, 2018, Proceedings / / edited by James H. Davenport, Manuel Kauers, George Labahn, Josef Urban |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XIX, 508 p. 132 illus.) |
| Disciplina | 510.285 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science—Mathematics
Discrete mathematics Artificial intelligence Data protection Computer programming Compilers (Computer programs) Information storage and retrieval systems Discrete Mathematics in Computer Science Artificial Intelligence Data and Information Security Programming Techniques Compilers and Interpreters Information Storage and Retrieval |
| ISBN | 3-319-96418-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Logic -- Number theory -- Combinatorics -- Algebra -- Analysis -- Geometry -- Inter-disciplinary -- Mathematical problem solving platform. |
| Record Nr. | UNINA-9910349418503321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||