LEADER 01063nam0-2200373---450- 001 990008651720403321 005 20081111103704.0 010 $a978-0-8218-4474-8 035 $a000865172 035 $aFED01000865172 035 $a(Aleph)000865172FED01 035 $a000865172 100 $a20080423d2008----km-y0itay50------ba 101 0 $aeng 102 $aUS 105 $aa-------001yy 200 1 $aClassifyng spaces of sporadic groups$fD. J. Benson, S. D. Smith 210 $aProvidence$cAmerican Mathematical Society$dc2008 215 $axvi, 289 p.$d24 cm 225 1 $aMathematical surveys and monographs$v147 610 0 $aGruppi semplici 610 0 $aCoomologia di gruppi finiti 676 $a512.2$v22 700 1$aBenson,$bDavid$054407 701 1$aSmith,$bStephen D.$0503325 801 0$aIT$bUNINA$gRICA$2UNIMARC 901 $aBK 912 $a990008651720403321 952 $aC-46-(147$b23151$fMA1 959 $aMA1 962 $a20D08 962 $a20J06 996 $aClassifyng spaces of sporadic groups$9715391 997 $aUNINA LEADER 00895nam0-22002891i-450- 001 990003052670403321 005 20041004113712.0 035 $a000305267 035 $aFED01000305267 035 $a(Aleph)000305267FED01 035 $a000305267 100 $a20030910d--------km-y0itay50------ba 101 0 $aita 102 $aIT 200 1 $aDue saggi sull'organizzazione e il finanziamento della scuola statale$fCarlo Buratti 225 1 $aDiscussion Papers$fDipartimento di Economia, Universitą degli studi di Trento$v93.11 610 0 $aIstruzione$aItalia 676 $a336$v11 rid.$zita 700 1$aBuratti,$bCarlo$0121285 801 0$aIT$bUNINA$gRICA$2UNIMARC 901 $aBK 912 $a990003052670403321 952 $aC 344$bs.i.$fDSS 959 $aDSS 959 $aSES 996 $aDue saggi sull'organizzazione e il finanziamento della scuola statale$9465704 997 $aUNINA LEADER 10440nam 22007695 450 001 9910483731403321 005 20251128114856.0 010 $a3-319-24246-6 024 7 $a10.1007/978-3-319-24246-0 035 $a(CKB)4340000000001115 035 $a(SSID)ssj0001585129 035 $a(PQKBManifestationID)16264715 035 $a(PQKBTitleCode)TC0001585129 035 $a(PQKBWorkID)14865252 035 $a(PQKB)11524308 035 $a(DE-He213)978-3-319-24246-0 035 $a(MiAaPQ)EBC6288143 035 $a(MiAaPQ)EBC5587900 035 $a(Au-PeEL)EBL5587900 035 $a(OCoLC)921999979 035 $a(PPN)190528478 035 $a(EXLCZ)994340000000001115 100 $a20150919d2015 u| 0 101 0 $aeng 135 $aurnn|008mamaa 181 $ctxt 182 $cc 183 $acr 200 10$aFrontiers of Combining Systems $e10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015, Proceedings /$fedited by Carsten Lutz, Silvio Ranise 205 $a1st ed. 2015. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2015. 215 $a1 online resource (XVII, 357 p. 54 illus. in color.) 225 1 $aLecture Notes in Artificial Intelligence,$x2945-9141 ;$v9322 300 $aIncludes index. 311 08$a3-319-24245-8 327 $aIntro -- 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 Go?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-Scho?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. 327 $a2.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. 327 $aRewriting 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. 327 $a1 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. 330 $aThis 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. . 410 0$aLecture Notes in Artificial Intelligence,$x2945-9141 ;$v9322 606 $aArtificial intelligence 606 $aMachine theory 606 $aComputer science 606 $aComputer programming 606 $aArtificial Intelligence 606 $aFormal Languages and Automata Theory 606 $aComputer Science Logic and Foundations of Programming 606 $aProgramming Techniques 615 0$aArtificial intelligence. 615 0$aMachine theory. 615 0$aComputer science. 615 0$aComputer programming. 615 14$aArtificial Intelligence. 615 24$aFormal Languages and Automata Theory. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aProgramming Techniques. 676 $a511.3 702 $aLutz$b Carsten$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aRanise$b Silvio$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910483731403321 996 $aFrontiers of Combining Systems$92555154 997 $aUNINA