Frontiers of Combining Systems [[electronic resource] ] : 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings / / edited by Carsten Lutz, Silvio Ranise

• Pubblicazione: Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015
• Edizione: 1st ed. 2015.
• Descrizione fisica: 1 online resource (XVII, 357 p. 54 illus. in color.)
• Disciplina: 511.3
• Soggetto topico: Artificial intelligence; Mathematical logic; Computer logic; Computer programming; Artificial Intelligence; Mathematical Logic and Formal Languages; Logics and Meanings of Programs; Programming Techniques
• Persona (resp. second.): LutzCarsten; RaniseSilvio
• Note generali: Includes index.
• 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.
• Sommario/riassunto: This book constitutes the proceedings of the 10th International Symposium on Frontiers of Combining Systems, FroCoS 2015, held in Wroclaw, Poland, in September 2015. The 20 papers presented in this volume were carefully reviewed and selected from 34 submissions. They were organized in topical sections named: description logics; theorem proving and model building; decision procedures; decision procedures for verification; rewriting and constraint solving; transformations between symbolic systems; combination methods; and reasoning in large theories. The book also contains one invited talk in full-paper length. .
• Titolo autorizzato: Frontiers of Combining Systems
• ISBN: 3-319-24246-6
• Formato: Materiale a stampa
• Livello bibliografico: Monografia
• Lingua di pubblicazione: Inglese
• Record Nr.: 996466470503316
• Lo trovi qui: Univ. di Salerno
• Serie: Lecture Notes in Artificial Intelligence ; ; 9322