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.
16th International Symposium on Temporal Representation and Reasoning : proceedings : Bressanone-Brixen, Italy 23-25 July 2009
| 16th International Symposium on Temporal Representation and Reasoning : proceedings : Bressanone-Brixen, Italy 23-25 July 2009 |
| Pubbl/distr/stampa | [Place of publication not identified], : IEEE Computer Society, 2009 |
| Soggetto topico |
Artificial intelligence
Reasoning Time Temporal databases Engineering & Applied Sciences Computer Science |
| ISBN | 1-5090-7514-3 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996212389203316 |
| [Place of publication not identified], : IEEE Computer Society, 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
16th International Symposium on Temporal Representation and Reasoning : proceedings : Bressanone-Brixen, Italy 23-25 July 2009
| 16th International Symposium on Temporal Representation and Reasoning : proceedings : Bressanone-Brixen, Italy 23-25 July 2009 |
| Pubbl/distr/stampa | [Place of publication not identified], : IEEE Computer Society, 2009 |
| Soggetto topico |
Artificial intelligence
Reasoning Time Temporal databases Engineering & Applied Sciences Computer Science |
| ISBN |
9781509075140
1509075143 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910138925903321 |
| [Place of publication not identified], : IEEE Computer Society, 2009 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Description Logic, Theory Combination, and All That [[electronic resource] ] : Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday / / edited by Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, Frank Wolter
| Description Logic, Theory Combination, and All That [[electronic resource] ] : Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday / / edited by Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, Frank Wolter |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XIII, 662 p. 1230 illus., 14 illus. in color.) |
| Disciplina | 006.332 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Artificial intelligence Computer science Information technology—Management Software engineering Computer networks Formal Languages and Automata Theory Artificial Intelligence Computer Science Logic and Foundations of Programming Computer Application in Administrative Data Processing Software Engineering Computer Communication Networks |
| ISBN | 3-030-22102-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | A Tour of Franz Baader's Contributions to Knowledge Representation and Automated Deduction -- Hierarchic Superposition Revisited -- Theory Combination: Beyond Equality Sharing -- Initial Steps Towards a Family of Regular-Like Plan Description Logics -- Reasoning with Justifiable Exceptions in EL_\bot Contextualized Knowledge Repositories -- Strong Explanations for Nonmonotonic Reasoning -- A KLM Perspective on Defeasible Reasoning for Description Logics -- Temporal Logic Programs with Temporal Description Logic Axioms -- The What-To-Ask Problem for Ontology-Based Peers -- From Model Completeness to Verification of Data Aware Processes -- Situation Calculus meets Description Logics -- Provenance Analysis: A Perspective for Description Logics? -- Extending EL^++ with Linear Constraints on the Probability of Axioms -- Effective query answering with Ontologies and DBoxes -- Checking the Data Complexity of Ontology-Mediated Queries: a Case Study with Non-Uniform CSPs and Polyanna -- Perceptual Context in Cognitive Hierarchies -- Do Humans Reason with E-Matchers? -- Pseudo-contractions as gentle repairs -- FunDL: A Family of Feature-Based Description Logics, with Applications in Querying Structured Data Sources -- Some Thoughts on Forward Induction in Multi-Agent-Path Finding Under Destination Uncertainty -- Temporally Attributed Description Logics -- Explaining Axiom Pinpointing -- Asymmetric Unification and Disunification -- Building and Combining Matching Algorithms -- Presburger Concept Cardinality Constraints in Very Expressive Description Logics -- A Note on Unification, Subsumption and Unification Type -- 15 Years of Consequence-Based Reasoning -- Maximum Entropy Calculations for the Probabilistic Description Logic ALC^ME -- Automating Automated Reasoning: The Case of Two Generic Automated Reasoning Tools -- On Bounded-Memory Stream Data Processing with Description Logics. |
| Record Nr. | UNISA-996466307203316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Description Logic, Theory Combination, and All That : Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday / / edited by Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, Frank Wolter
| Description Logic, Theory Combination, and All That : Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday / / edited by Carsten Lutz, Uli Sattler, Cesare Tinelli, Anni-Yasmin Turhan, Frank Wolter |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XIII, 662 p. 1230 illus., 14 illus. in color.) |
| Disciplina |
006.332
005.1015113 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Artificial intelligence Computer science Information technology—Management Software engineering Computer networks Formal Languages and Automata Theory Artificial Intelligence Computer Science Logic and Foundations of Programming Computer Application in Administrative Data Processing Software Engineering Computer Communication Networks |
| ISBN | 3-030-22102-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | A Tour of Franz Baader's Contributions to Knowledge Representation and Automated Deduction -- Hierarchic Superposition Revisited -- Theory Combination: Beyond Equality Sharing -- Initial Steps Towards a Family of Regular-Like Plan Description Logics -- Reasoning with Justifiable Exceptions in EL_\bot Contextualized Knowledge Repositories -- Strong Explanations for Nonmonotonic Reasoning -- A KLM Perspective on Defeasible Reasoning for Description Logics -- Temporal Logic Programs with Temporal Description Logic Axioms -- The What-To-Ask Problem for Ontology-Based Peers -- From Model Completeness to Verification of Data Aware Processes -- Situation Calculus meets Description Logics -- Provenance Analysis: A Perspective for Description Logics? -- Extending EL^++ with Linear Constraints on the Probability of Axioms -- Effective query answering with Ontologies and DBoxes -- Checking the Data Complexity of Ontology-Mediated Queries: a Case Study with Non-Uniform CSPs and Polyanna -- Perceptual Context in Cognitive Hierarchies -- Do Humans Reason with E-Matchers? -- Pseudo-contractions as gentle repairs -- FunDL: A Family of Feature-Based Description Logics, with Applications in Querying Structured Data Sources -- Some Thoughts on Forward Induction in Multi-Agent-Path Finding Under Destination Uncertainty -- Temporally Attributed Description Logics -- Explaining Axiom Pinpointing -- Asymmetric Unification and Disunification -- Building and Combining Matching Algorithms -- Presburger Concept Cardinality Constraints in Very Expressive Description Logics -- A Note on Unification, Subsumption and Unification Type -- 15 Years of Consequence-Based Reasoning -- Maximum Entropy Calculations for the Probabilistic Description Logic ALC^ME -- Automating Automated Reasoning: The Case of Two Generic Automated Reasoning Tools -- On Bounded-Memory Stream Data Processing with Description Logics. |
| Record Nr. | UNINA-9910337835703321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Frontiers of Combining Systems [[electronic resource] ] : 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings / / edited by Carsten Lutz, Silvio Ranise
| Frontiers of Combining Systems [[electronic resource] ] : 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings / / edited by Carsten Lutz, Silvio Ranise |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XVII, 357 p. 54 illus. in color.) |
| Disciplina | 511.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Mathematical logic Computer logic Computer programming Artificial Intelligence Mathematical Logic and Formal Languages Logics and Meanings of Programs Programming Techniques |
| ISBN | 3-319-24246-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Abstracts of Invited Talks -- Contents -- Invited Talk -- Free Variables and Theories: Revisiting Rigid E-Unification -- 1 Introduction -- 2 Background -- 2.1 Rigid E-Unification -- 2.2 Subterm Instantiation and Bounded Rigid E-Unification -- 2.3 Bounded Rigid E-Unification Formally -- 3 Semantically Solving BREU -- 3.1 Semantic Solvability in a First-Order Calculus -- 3.2 The Complexity of Semantic Solvability -- 4 Towards Bounded Rigid Theory Unification -- 5 Challenges and Conclusion -- Description Logics -- Decidable Description Logics of Context with Rigid Roles -- 1 Introduction -- 2 Basic Notions -- 3 Complexity of the Consistency Problem -- 4 The Case of EL: LM[[EL]] and EL[[LO]] -- 5 Conclusions -- Adding Threshold Concepts to the Description Logic EL -- 1 Introduction -- 2 The Description Logic EL -- 3 The Logic EL(m) -- 4 The Membership Function deg -- 5 Reasoning in EL(deg) -- 6 Concept Similarity and Relaxed Instance Queries -- 7 Conclusion -- Reasoning in Expressive Description Logicsunder Infinitely Valued Gödel Semantics -- 1 Introduction -- 2 Preliminaries -- 3 Automata for Complex Role Inclusions -- 4 The Reduction -- 5 Conclusions -- References -- Theorem Proving and Model Building -- NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment -- 1 Introduction -- 2 Preliminaries -- 3 Calculus -- 4 Soundness -- 5 Termination and Completeness -- 6 Related Work -- 7 Conclusion -- First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation -- 1 Introduction -- 2 Linear Shallow Monadic Horn Approximation -- 3 Lifting a Conflicting Core -- 4 Approximation Refinement -- 5 Summary -- An Expressive Model for Instance Decomposition Based Parallel SAT Solvers -- 1 Introduction -- 2 Background -- 2.1 The Satisfiability Problem.
2.2 Partition Functions in SAT Solvers -- 2.3 Label Functions -- 3 The Instance Decomposition Model ID -- 4 Proof Format -- 5 Conclusion -- Decision Procedures -- Weakly Equivalent Arrays -- 1 Introduction -- 2 Notation -- 3 A Motivating Example -- 4 Weak Equivalences over Arrays -- 5 A Decision Procedure Based on Weak Equivalences -- 6 Extension to TAxDiff -- 7 Implementation and Evaluation -- 8 Conclusion and Future Work -- A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings -- 1 Introduction -- 1.1 Related Work -- 1.2 Formal Preliminaries -- 2 A Theory of Strings and Regular Language Membership -- 3 A Calculus for Constraint Satisfiability in TLR -- 4 Calculus Correctness -- 4.1 Termination -- 4.2 Correctness -- 4.3 Decidability -- 5 Conclusion and Further Work -- Adapting Real Quantifier Elimination Methods for Conflict Set Computation -- 1 Introduction -- 2 Real Quantifier Elimination -- 2.1 Cylindrical Algebraic Decomposition -- 2.2 Virtual Substitution -- 3 Finding Conflict Sets -- 3.1 Conflict Sets and Linear Programming -- 3.2 Conflict Sets and Quantifier Elimination Optimization -- 4 Finding Conflict Sets via Redlog -- 5 Conclusion -- Decision Procedures for Verification -- A New Acceleration-Based Combination Framework for Array Properties -- 1 Introduction -- 2 Notation -- 3 Acceleratable Fragments -- 4 Acceleration Modules in Satisfiability Procedures -- 5 Applications to Imperative Programs -- 6 Conclusions and Future Work -- Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata -- 1 Introduction -- 2 Spatial Families of Hybrid Automata -- 3 Verification Tasks -- 3.1 Safety Properties -- 3.2 Reduction to Satisfiability Checking -- 4 Automated Reasoning -- 5 Verification: Decidability and Complexity -- 6 Tool Support -- 7 Conclusions. Rewriting and Constraint Solving -- A Completion Method to Decide Reachabilityin Rewrite Systems -- 1 Introduction -- 2 Polarized Rewrite Systems -- 3 Cut-Elimination -- 4 Ground Finite Rewrite Systems -- 5 Pushdown Systems -- Axiomatic Constraint Systemsfor Proof Search Modulo Theories -- 1 Introduction -- 2 Ground Calculus and Examples -- 3 Constraint Structures -- 4 A System for Proof Search with Constraints -- 4.1 The Constraint-Producing Sequent Calculus LK?1 -- 4.2 Instantiations and Compatibility with Constraints -- 4.3 Soundness and Completeness -- 5 Sequentialising -- 5.1 Definition of the Proof System -- 5.2 Soundness and Completeness -- 6 Relating LK?"526930B 1 to LK1 -- 7 Implementation -- 8 Related Works and Further Work -- Transformations between SymbolicSystems -- Formalizing Soundness and Completeness of Unravelings -- 1 Introduction -- 2 Preliminaries -- 3 Formalizing Conditional Rewriting -- 4 Unravelings -- 5 Completeness of Unravelings -- 6 Soundness of Unravelings -- 7 Applying Unravelings to Confluence -- 8 Conclusion -- Proofs and Reconstructions -- 1 Introduction -- 2 Reconstruction Workflow -- 3 Cut Machines -- 3.1 Validating the Model -- 3.2 Using the Model -- 3.3 Extending the Model -- 4 Framework -- 4.1 Proof Generation -- 4.2 Formula Interpretation -- 4.3 Proof Analysis and Transformation -- 4.4 Emulation of Inference Rules -- 4.5 Generating a Cut Program -- 4.6 Executing a Cut Program -- 5 Implementation -- 5.1 Evaluation -- 6 Related Work -- 7 Conclusions -- Combination Methods -- A Rewriting Approach to the Combination of Data Structures with Bridging Theories -- 1 Introduction -- 2 Preliminaries: Notations and Combinations -- 3 Combination with Bridging Theories -- 4 Basic Data Structure Theories -- 5 Completeness Proof -- 6 Conclusion -- Unification and Matching in Hierarchical Combinations of Syntactic Theories. 1 Introduction -- 2 Preliminaries -- 3 Hierarchical Combination -- 3.1 Combination Procedure for Hierarchical Combination -- 4 Unification in Shallow Hierarchical Combination -- 5 Matching in Finite Syntactic Hierarchical Combination -- 5.1 Mutation-Based Procedure -- 5.2 Combination Procedure -- 5.3 Example: Matching in a Theory of Distributive Exponentiation -- 6 Conclusion -- Combining Forward and Backward Propagation -- 1 Introduction -- 2 Constraint Handling Rules -- 2.1 Syntax -- 2.2 Operational Forward Semantics -- 2.3 Operational Backwards Semantics -- 3 Combined CHR Programs -- 3.1 General Formulation -- 3.2 Forward CHR -- 3.3 Backward CHR -- 4 Interleaved Forward/Backward Propagation -- 5 Application for Combined Programs -- 5.1 Modeling -- 5.2 Strictly Forward -- 5.3 Strictly Backward -- 6 Conclusion -- Reasoning in Large Theories -- Random Forests for Premise Selection -- 1 Introduction -- 2 Premise Selection -- 2.1 Quality Measures -- 2.2 Evaluation -- 2.3 Used Datasets -- 3 Existing Algorithms -- 4 Adaptations to Random Forests for Premise Selection -- 4.1 Sample Selection -- 4.2 Incremental Update -- 4.3 Tree Size -- 4.4 Feature Selection -- 4.5 Querying a Tree -- 4.6 Querying a Forest -- 5 Experiments -- 6 Conclusion -- Lemmatization for Stronger Reasoning in Large Theories -- 1 Introduction -- 2 Lemmatization Scenario and Initial Statistics -- 3 Extracting Reusable Lemmas from Refutational Proofs -- 3.1 Extracting Lemmas from the Natural Deduction Proofs -- 4 Filtering Lemmas -- 4.1 Additional Filters -- 5 Problem-Specific Premise Selection -- 6 Evaluation -- 7 Examples of New Lemmas -- 8 Related Work -- 9 Conclusion and Future Work -- Author Index. |
| Record Nr. | UNISA-996466470503316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Frontiers of Combining Systems : 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings / / edited by Carsten Lutz, Silvio Ranise
| Frontiers of Combining Systems : 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings / / edited by Carsten Lutz, Silvio Ranise |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XVII, 357 p. 54 illus. in color.) |
| Disciplina | 511.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Mathematical logic Computer logic Computer programming Artificial Intelligence Mathematical Logic and Formal Languages Logics and Meanings of Programs Programming Techniques |
| ISBN | 3-319-24246-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Abstracts of Invited Talks -- Contents -- Invited Talk -- Free Variables and Theories: Revisiting Rigid E-Unification -- 1 Introduction -- 2 Background -- 2.1 Rigid E-Unification -- 2.2 Subterm Instantiation and Bounded Rigid E-Unification -- 2.3 Bounded Rigid E-Unification Formally -- 3 Semantically Solving BREU -- 3.1 Semantic Solvability in a First-Order Calculus -- 3.2 The Complexity of Semantic Solvability -- 4 Towards Bounded Rigid Theory Unification -- 5 Challenges and Conclusion -- Description Logics -- Decidable Description Logics of Context with Rigid Roles -- 1 Introduction -- 2 Basic Notions -- 3 Complexity of the Consistency Problem -- 4 The Case of EL: LM[[EL]] and EL[[LO]] -- 5 Conclusions -- Adding Threshold Concepts to the Description Logic EL -- 1 Introduction -- 2 The Description Logic EL -- 3 The Logic EL(m) -- 4 The Membership Function deg -- 5 Reasoning in EL(deg) -- 6 Concept Similarity and Relaxed Instance Queries -- 7 Conclusion -- Reasoning in Expressive Description Logicsunder Infinitely Valued Gödel Semantics -- 1 Introduction -- 2 Preliminaries -- 3 Automata for Complex Role Inclusions -- 4 The Reduction -- 5 Conclusions -- References -- Theorem Proving and Model Building -- NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment -- 1 Introduction -- 2 Preliminaries -- 3 Calculus -- 4 Soundness -- 5 Termination and Completeness -- 6 Related Work -- 7 Conclusion -- First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation -- 1 Introduction -- 2 Linear Shallow Monadic Horn Approximation -- 3 Lifting a Conflicting Core -- 4 Approximation Refinement -- 5 Summary -- An Expressive Model for Instance Decomposition Based Parallel SAT Solvers -- 1 Introduction -- 2 Background -- 2.1 The Satisfiability Problem.
2.2 Partition Functions in SAT Solvers -- 2.3 Label Functions -- 3 The Instance Decomposition Model ID -- 4 Proof Format -- 5 Conclusion -- Decision Procedures -- Weakly Equivalent Arrays -- 1 Introduction -- 2 Notation -- 3 A Motivating Example -- 4 Weak Equivalences over Arrays -- 5 A Decision Procedure Based on Weak Equivalences -- 6 Extension to TAxDiff -- 7 Implementation and Evaluation -- 8 Conclusion and Future Work -- A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings -- 1 Introduction -- 1.1 Related Work -- 1.2 Formal Preliminaries -- 2 A Theory of Strings and Regular Language Membership -- 3 A Calculus for Constraint Satisfiability in TLR -- 4 Calculus Correctness -- 4.1 Termination -- 4.2 Correctness -- 4.3 Decidability -- 5 Conclusion and Further Work -- Adapting Real Quantifier Elimination Methods for Conflict Set Computation -- 1 Introduction -- 2 Real Quantifier Elimination -- 2.1 Cylindrical Algebraic Decomposition -- 2.2 Virtual Substitution -- 3 Finding Conflict Sets -- 3.1 Conflict Sets and Linear Programming -- 3.2 Conflict Sets and Quantifier Elimination Optimization -- 4 Finding Conflict Sets via Redlog -- 5 Conclusion -- Decision Procedures for Verification -- A New Acceleration-Based Combination Framework for Array Properties -- 1 Introduction -- 2 Notation -- 3 Acceleratable Fragments -- 4 Acceleration Modules in Satisfiability Procedures -- 5 Applications to Imperative Programs -- 6 Conclusions and Future Work -- Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata -- 1 Introduction -- 2 Spatial Families of Hybrid Automata -- 3 Verification Tasks -- 3.1 Safety Properties -- 3.2 Reduction to Satisfiability Checking -- 4 Automated Reasoning -- 5 Verification: Decidability and Complexity -- 6 Tool Support -- 7 Conclusions. Rewriting and Constraint Solving -- A Completion Method to Decide Reachabilityin Rewrite Systems -- 1 Introduction -- 2 Polarized Rewrite Systems -- 3 Cut-Elimination -- 4 Ground Finite Rewrite Systems -- 5 Pushdown Systems -- Axiomatic Constraint Systemsfor Proof Search Modulo Theories -- 1 Introduction -- 2 Ground Calculus and Examples -- 3 Constraint Structures -- 4 A System for Proof Search with Constraints -- 4.1 The Constraint-Producing Sequent Calculus LK?1 -- 4.2 Instantiations and Compatibility with Constraints -- 4.3 Soundness and Completeness -- 5 Sequentialising -- 5.1 Definition of the Proof System -- 5.2 Soundness and Completeness -- 6 Relating LK?"526930B 1 to LK1 -- 7 Implementation -- 8 Related Works and Further Work -- Transformations between SymbolicSystems -- Formalizing Soundness and Completeness of Unravelings -- 1 Introduction -- 2 Preliminaries -- 3 Formalizing Conditional Rewriting -- 4 Unravelings -- 5 Completeness of Unravelings -- 6 Soundness of Unravelings -- 7 Applying Unravelings to Confluence -- 8 Conclusion -- Proofs and Reconstructions -- 1 Introduction -- 2 Reconstruction Workflow -- 3 Cut Machines -- 3.1 Validating the Model -- 3.2 Using the Model -- 3.3 Extending the Model -- 4 Framework -- 4.1 Proof Generation -- 4.2 Formula Interpretation -- 4.3 Proof Analysis and Transformation -- 4.4 Emulation of Inference Rules -- 4.5 Generating a Cut Program -- 4.6 Executing a Cut Program -- 5 Implementation -- 5.1 Evaluation -- 6 Related Work -- 7 Conclusions -- Combination Methods -- A Rewriting Approach to the Combination of Data Structures with Bridging Theories -- 1 Introduction -- 2 Preliminaries: Notations and Combinations -- 3 Combination with Bridging Theories -- 4 Basic Data Structure Theories -- 5 Completeness Proof -- 6 Conclusion -- Unification and Matching in Hierarchical Combinations of Syntactic Theories. 1 Introduction -- 2 Preliminaries -- 3 Hierarchical Combination -- 3.1 Combination Procedure for Hierarchical Combination -- 4 Unification in Shallow Hierarchical Combination -- 5 Matching in Finite Syntactic Hierarchical Combination -- 5.1 Mutation-Based Procedure -- 5.2 Combination Procedure -- 5.3 Example: Matching in a Theory of Distributive Exponentiation -- 6 Conclusion -- Combining Forward and Backward Propagation -- 1 Introduction -- 2 Constraint Handling Rules -- 2.1 Syntax -- 2.2 Operational Forward Semantics -- 2.3 Operational Backwards Semantics -- 3 Combined CHR Programs -- 3.1 General Formulation -- 3.2 Forward CHR -- 3.3 Backward CHR -- 4 Interleaved Forward/Backward Propagation -- 5 Application for Combined Programs -- 5.1 Modeling -- 5.2 Strictly Forward -- 5.3 Strictly Backward -- 6 Conclusion -- Reasoning in Large Theories -- Random Forests for Premise Selection -- 1 Introduction -- 2 Premise Selection -- 2.1 Quality Measures -- 2.2 Evaluation -- 2.3 Used Datasets -- 3 Existing Algorithms -- 4 Adaptations to Random Forests for Premise Selection -- 4.1 Sample Selection -- 4.2 Incremental Update -- 4.3 Tree Size -- 4.4 Feature Selection -- 4.5 Querying a Tree -- 4.6 Querying a Forest -- 5 Experiments -- 6 Conclusion -- Lemmatization for Stronger Reasoning in Large Theories -- 1 Introduction -- 2 Lemmatization Scenario and Initial Statistics -- 3 Extracting Reusable Lemmas from Refutational Proofs -- 3.1 Extracting Lemmas from the Natural Deduction Proofs -- 4 Filtering Lemmas -- 4.1 Additional Filters -- 5 Problem-Specific Premise Selection -- 6 Evaluation -- 7 Examples of New Lemmas -- 8 Related Work -- 9 Conclusion and Future Work -- Author Index. |
| Record Nr. | UNINA-9910483731403321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
KI 2014: Advances in Artificial Intelligence [[electronic resource] ] : 37th Annual German Conference on AI, Stuttgart, Germany, September 22-26, 2014, Proceedings / / edited by Carsten Lutz, Michael Thielscher
| KI 2014: Advances in Artificial Intelligence [[electronic resource] ] : 37th Annual German Conference on AI, Stuttgart, Germany, September 22-26, 2014, Proceedings / / edited by Carsten Lutz, Michael Thielscher |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XII, 321 p. 72 illus.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Information storage and retrieval Computer simulation User interfaces (Computer systems) Mathematical logic Artificial Intelligence Information Storage and Retrieval Simulation and Modeling User Interfaces and Human Computer Interaction Mathematical Logic and Formal Languages |
| ISBN | 3-319-11206-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Cognitive Modeling -- Computer Vision -- Constraint Satisfaction, Search, and Optimization -- Knowledge Representation and Reasoning -- Machine Learning and Data Mining -- Planning and Scheduling. |
| Record Nr. | UNISA-996199684103316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
KI 2014: Advances in Artificial Intelligence : 37th Annual German Conference on AI, Stuttgart, Germany, September 22-26, 2014, Proceedings / / edited by Carsten Lutz, Michael Thielscher
| KI 2014: Advances in Artificial Intelligence : 37th Annual German Conference on AI, Stuttgart, Germany, September 22-26, 2014, Proceedings / / edited by Carsten Lutz, Michael Thielscher |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XII, 321 p. 72 illus.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Information storage and retrieval Computer simulation User interfaces (Computer systems) Mathematical logic Artificial Intelligence Information Storage and Retrieval Simulation and Modeling User Interfaces and Human Computer Interaction Mathematical Logic and Formal Languages |
| ISBN | 3-319-11206-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Cognitive Modeling -- Computer Vision -- Constraint Satisfaction, Search, and Optimization -- Knowledge Representation and Reasoning -- Machine Learning and Data Mining -- Planning and Scheduling. |
| Record Nr. | UNINA-9910484850303321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||