Note: Intro -- Preface -- Organization -- Table of Contents -- Query-Answering Systems -- Conceptual Pathway Querying of Natural Logic Knowledge Bases from Text Bases -- 1 Introduction -- 2 Deductive Querying of Knowledge Bases -- 2.1 Deducing Relationships -- 3 The Graph Knowledge Base View -- 3.1 Deducing Pathways -- 4 Natural Logic -- 4.1 Non-monotonic Logic in Natural Logic -- 5 From Natural Language to Natural Logic -- 5.1 Example -- 6 Flattening Natural Logic into Clauses -- 7 Inference Engine for Conceptual Pathfinding -- 8 Summary and Conclusion -- References -- Query Rewriting for an Incremental Search in Heterogeneous Linked Data Sources -- 1 Introduction -- 2 Related Works -- 3 An Overview of the Query Processing Approach -- 3.1 Main Query Processing Steps -- 3.2 System Modules -- 4 Query Rewriting Algorithm -- 5 Estimation of Information Loss -- 5.1 Measuring the Loss of Information -- 5.2 Rewriting Example -- 6 Conclusions -- References -- FILT - Filtering Indexed Lucene Triples - A SPARQL Filter Query Processing Engine- -- 1 Introduction -- 2 Implementation of FILT with Apache Lucene -- 3 Previous Work -- 4 Benchmark Evaluation -- 5 Results -- 6 Discussion -- 7 Conclusions and Future Work -- References -- Improving Range Query Result Size Estimation Based on a New Optimal Histogram -- 1 Introduction -- 2 State of the Art -- 2.1 Earlier Histograms -- 2.2 Relative Recent Histograms -- 3 Compressed-V2 Histogram -- 3.1 Definitions and Problem Formulation -- 3.2 HistConst Algorithm -- 4 Running Example -- 4.1 Selectivity Estimation of Low Frequent Values with Compressed andCompressed-v2 Histograms -- 5 Experimentation Results -- 6 Conclusion and Future Work -- References -- Has FQAS Something to Say on Taking Good Care of Our Elders? -- 1 Introduction -- 2 Knowledge Representation and Information Retrieval. , 3 Domain and User Context Modelling -- 4 Approximate Reasoning Models -- 4.1 Activity Recognition -- 5 Human Computer Interaction -- 5.1 Social Networks -- 6 Conclusions -- References -- Question Answering System for Dialogues: A New Taxonomy of Opinion Questions -- 1 Introduction -- 2 Related Works -- 2.1 Question Type Taxonomies -- 2.2 Opinion Extraction Techniques -- 2.3 Question Classification Approaches -- 3 Proposed Taxonomy for Opinion Question Classification -- 3.1 Building the Study Corpus -- 3.2 Question Specificities of QAS for Dialogues -- 3.3 Proposed Taxonomy for Opinion Questions -- 3.4 Discussions about the Proposed Taxonomy -- 4 Proposed Approach for the Opinion Question Classification -- 4.1 Extraction of Classification Features -- 4.2 Training Corpus -- 4.3 Results and Discussions -- 5 Conclusion and Perspectives -- References -- R/quest: A Question Answering System -- 1 Introduction and Related Work -- 2 R/quest Methodology -- 2.1 Answer Retrieval Using Question Expansion -- 2.2 Candidate Answer Ranking -- 2.3 Question Refinement -- 3 Evaluation -- 4 Conclusion -- 5 Future Work -- References -- Answering Questions by Means of Causal Sentences -- 1 Introduction -- 2 Selection of the Input Information -- 3 Summarizing the Content of the Causal Graph -- 4 Conclusions and Future Works -- References -- Ontology-Based Question Analysis Method -- 1 Introduction -- 2 Related Works -- 3 Question Analysis Method -- 3.1 Proposed Method's Description -- 3.2 Lexical and Syntactic Analysis Component -- 3.3 Question Graph Construction Component -- 3.4 Query Reformulation Component -- 3.5 Search for Similar Questions -- 4 Experimental Evaluation -- 4.1 Search Results Evaluation -- 4.2 Similar Question Search Evaluation -- 5 Conclusion -- References -- Fuzzy Multidimensional Modelling for Flexible Querying of Learning Object Repositories. , 1 Introduction -- 2 Background and Motivation -- 2.1 LOs, LORs and LO Metadata -- 2.2 Datawarehousing, OLAP and OLTP -- 2.3 Fuzzy Sets Theory and OLAP -- 2.4 Need for DW Techniques in LORs -- 3 Learning Object Metadata Standards -- 4 A Fuzzy Multidimensional Model of Learning Object Repositories -- 4.1 The Fuzzy Dimensions -- 4.2 An Example Datacube -- 5 Conclusions and Future Work -- References -- Environmental Scanning for Strategic Early Warning -- Using Formal Concept Analysis to Detect and Monitor Organised Crime -- 1 Introduction -- 2 Formal Concept Analysis -- 2.1 Formal Contexts -- 2.2 Formal Concepts -- 2.3 Galois Connections -- 2.4 Concept Lattices -- 2.5 Representing Organised Crime with FCA -- 3 Detecting OC Activities -- 4 Finding OC Dependencies -- 5 Finding New Indicators for OC -- 6 Conclusion: Developing an OC `Threat Score Card' -- References -- Analysis of Semantic Networks Using Complex Networks Concepts -- 1 Introduction -- 2 Related Work -- 3 Finding the Most Important Terms in a Semantic Network -- 4 Experimental Results -- 5 Conclusions -- References -- Detecting Anomalous and Exceptional Behaviour on Credit Data by Means of Association Rules -- 1 Introduction -- 2 Background Concepts and Related Work -- 2.1 Association Rules -- 2.2 Related Works -- 3 Previous Approaches for Discovering Exception and Anomalous Rules -- 4 Our Proposal for Mining Exception and Anomalous Rules -- 4.1 Our Approach for Exception Rules -- 4.2 Our Approach for Anomalous Rules -- 5 Algorithm -- 6 Experimental Evaluation -- 7 Conclusions and Future Research -- References -- Issues of Security and Informational Privacy in Relation to an Environmental Scanning System for Fighting Organized Crime -- 1 Introduction -- 2 Aims of the ePOOLICE Project -- 3 Balancing Security and Privacy -- 4 Privacy Issues in ePOOLICE -- 5 Concluding Remarks -- References. , Semantic Technology -- Algorithmic Semantics for Processing Pronominal Verbal Phrases -- 1 Background and Recent Developments -- 1.1 Algorithmic Intensionality in the Type Theory Lar -- 1.2 Restricted -reduction in Lar and Pronominal Underspecification -- 2 VP Ellipsis and Underspecification -- 3 Question-Answer Interaction with Underspecified Answers -- 4 Ongoing and Future Work -- 5 Conclusions -- References -- Improving the Understandability of OLAP Queries by Semantic Interpretations -- 1 Introduction -- 2 Multidimensional Model -- 2.1 Multidimensional Structure -- 2.2 Operations -- 3 Semantic Interpretation -- 3.1 Structure -- 3.2 Aggregation Functions -- 4 Semantic Interpretations for DataCubes -- 4.1 Query Process -- 4.2 Learning the fa Functions -- 5 Example -- 6 Conclusions -- References -- Semantic Interpretation of Intermediate Quantifiers and Their Syllogisms -- 1 Introduction -- 2 Basic Concepts of the Fuzzy Type Theory -- 3 Theory of Intermediate Quantifiers -- 4 Generalized Intermediate Syllogisms -- 4.1 Interpretation -- 4.2 Examples of Strongly Valid Syllogisms of Figure I -- 4.3 Examples of Strongly Valid Syllogisms of Figure II -- 4.4 Examples of Strongly Valid Syllogisms of Figure-III -- 4.5 Example of Invalid Syllogism -- 5 Conclusions -- References -- Ranking Images Using Customized Fuzzy Dominant Color Descriptors -- 1 Introduction -- 2 Fuzzy Modelling of Colors -- 2.1 Fuzzy Color -- 2.2 Fuzzy Color Space -- 3 Dominance-Based Fuzzy Color Descriptor -- 3.1 Dominant Fuzzy Colors -- 3.2 Dominance-Based Fuzzy Descriptors -- 4 Matching Operators -- 4.1 Fuzzy Inclusion Operator -- 5 Results -- 5.1 Customized Color Space: An Example -- 5.2 Query Refinement Examples -- 6 Conclusions -- References -- Generating Linguistic Descriptions of Data -- Linguistic Descriptions: Their Structure and Applications. , 1 Introduction - Necessity to Learn from Linguists and Logicians -- 2 Theory of Evaluative Linguistic Expressions -- 2.1 Grammatical Structure of Evaluative Expressions -- 2.2 Semantics of Simple Evaluative Expressions -- 3 Linguistic Descriptions and Their Semantics -- 3.1 The Concept of a Linguistic Description -- 3.2 Semantics of Linguistic Description -- 3.3 Learning of Linguistic Description from Data -- 3.4 Perception-Based Logical Deduction -- 4 Linguistic Descriptions in the Analysis and Forecasting of Time Series -- 5 Mining Linguistic Associations -- 5.1 The Original Method -- 6 Other Applications and Conclusion -- References -- Landscapes Description Using Linguistic Summaries and a Two-Dimensional Cellular Automaton -- 1 Introduction -- 2 Background -- 2.1 Cellular Automata -- 2.2 Linguistic Summaries of Data -- 3 Linguistic Summary of Individual Behavior -- 3.1 Inferring an Instance of a State Machine Instance -- 3.2 Obtaining a Linguistic Summary from a State Machine Instance -- 4 Global Description of the Landscape Situation -- 4.1 Landscape Division -- 4.2 Definition of the Basic Measures -- 4.3 Define the First Order Perceptions -- 4.4 Definition of the Top-Order Perceptions -- 5 Conclusions and Future Work -- References -- Comparing f-Optimal with Distance Based Merge Functions -- 1 Introduction -- 2 Preliminaries -- 2.1 Multisets -- 2.2 Merge Functions -- 3 Influencing the Content Selection -- 4 Distance Based Merge Functions -- 5 Making the Comparison -- 5.1 Properties -- 5.2 Multi-Document Summarization -- 6 Conclusion and Future Work -- References -- Flexible Querying with Linguistic F-Cube Factory -- 1 Introduction -- 2 Preliminary Research -- 2.1 Multidimensional Data Model and F-Cube Factory -- 2.2 Linguistic Comparison of Time Series Data -- 3 Linguistic F-Cube Factory -- 4 Conclusions and Future Work -- References. , Mathematical Morphology Tools to Evaluate Periodic Linguistic Summaries.

Note: Intro -- Title -- Preface -- Organization -- Contents -- Information and Knowledge Management -- Knowledge Acquisition Activity in Software Development -- Introduction -- Information Source Model -- Field Studies -- Data Acquisition Approach -- Knowledge Acquisition in Software Projects -- Concluding Remarks -- References -- An Electronic Learning System for Integrating Knowledge Management and Alumni Systems -- Introduction -- Electronic Learning and Knowledge Management -- Electronic Learning -- Knowledge Management -- System Framework and Implementation -- Case Study -- Alumni System Components -- Knowledge Management Components -- System Analysis and Proposed Framework -- System Design and Implementation -- System Evaluation -- Conclusion -- References -- Knowledge Management Systems and Intellectual Capital Measurement in Portuguese Organizations: A Case Study -- Introduction -- Background -- Intellectual Capital Measurement Models -- Knowledge Management Systems -- Research Methodology -- Results and Discussion -- Knowledge Management Systems -- Intellectual Capital Measurement -- Conclusions -- References -- Semantic Patent Information Retrieval and Management with OWL -- Introduction -- Related Work -- Semantic Information Retrieval from XML to OWL -- Method for Transforming XML into OWL with Stylesheets -- Structure of the Hierarchical Codes -- Customization of the Stylesheets for Hierarchical Codes -- Reasoning through Ontology Hierarchy -- Conclusions -- References -- Multilevel Clustering of Induction Rules for Web Meta-knowledge -- Introduction -- Knowledge Mining -- Knowledge Representation -- Induction Rules -- A Distance Measure for Knowledge Rules -- Centroids Computation -- Multilevel Induction Rules Clustering -- Related Works of Multilevel Paradigm -- The Proposed Algorithm -- Coarsening Step -- The Initial Solution. , The Refinement Step -- Evaluation and Experimentation -- Benchmark Construction -- Evaluation Pattern -- Experimentation -- Conclusion -- References -- Knowledge-Based Risk Management: Survey on Brazilian Software Development Enterprises -- Introduction -- Literature Review -- Incubators and Technological Incubated and Graduated Based Enterprises -- Risk Management and the Relationship with Knowledge Management -- Research Method -- Results Obtained and Analyzes -- Obtained Results -- Data Analysis through Partial Least Square (PLS) -- Conclusions -- References -- Leveraging Knowledge from Different Communities Using Ontologies -- Introduction - Leveraging Knowledge -- Knowledge and Common Ontology -- Implementing the Solution -- How to Get Common Terms - Common Ontology (CO) -- Implementation -- Testing Queries -- Conclusions -- References -- An Approach for Deriving Semantically Related Category Hierarchies from Wikipedia Category Graphs -- Introduction -- Related Work -- Methodology -- Pre-processing -- Algorithm -- Evaluation -- Building the Evaluation Dataset -- Results -- Analysis -- Conclusion -- References -- Privacy Policies in Web Sites of Portuguese Municipalities: An Empirical Study -- Introduction -- Related Work -- Methods -- Results and Discussion -- Conclusions and Future Work -- References -- Knowledge Integration in Problem Solving Processes -- Introduction -- Knowledge Integration Process -- Knowledge Concept -- Knowledge Sharing and Integration -- Methodology -- Research Methodology -- Data Analysis -- Research Findings -- Problem Solving in Alpha Organisation -- Knowledge Integration in Problem Solving Processes -- Conclusions -- References -- Collaborative Elicitation of Conceptual Representations: A Corpus-Based Approach -- Introduction -- Related Work -- Collaboration in Knowledge Representation. , Supporting Conceptualisation Processes: The ConceptME Approach -- Conceptualisation Framework (CF) -- An Overview of the ConceptME -- Corpus-Based Conceptual Modelling: Describing the Architecture -- Results -- Conclusions -- References -- Effect of Demography on Mobile Commerce Frequency of Actual Use in Saudi Arabia -- Introduction -- Demographic Differences -- Gender -- Age -- Education -- Research Methodology -- The Survey Instrument Development -- Sample Demographic Profile of Participants -- Discussion -- Conclusion -- References -- Specialized Knowledge Systems - A Model for Intelligent Learning Management within Organizations -- Introduction -- Research Problem -- Social Semantic Web: Trends and Potentialities for New e-Learning Environments -- Behavioral and Learning Trends in the Digital Era -- Conceptual Model -- Conclusions -- References -- How Small and Medium Enterprises Are Using Social Networks? Evidence from the Algarve Region -- Introduction -- The Alignment Issue -- An Empirical Study -- Sample and Methodology -- Analysis of Patterns -- Discussion and Implications -- Conclusions -- References -- Temporal Visualization of a Multidimensional Network of News Clips -- Introduction -- Reference Work -- DataSet -- Multidimensional Network of News Clips -- Visualization System -- Multidimensional Network Visualization -- Index and Search -- Event Detection -- Graph Navigation -- Discussion -- Conclusions and Future Work -- References -- User Documentation: The Cinderella of Information Systems -- The Case for User Documentation -- "Well-Designed Software Needs No Documentation" -- "Nobody Reads Documentation, Anyhow" -- Designing Documentation -- Stuck in a Rut -- Wanted: Research -- References -- Task Topic Knowledge vs. Background Domain Knowledge: Impact of Two Types of Knowledge on User Search Performance -- Introduction. , Related Work -- Domain Knowledge -- Search Task Topic Knowledge -- Methodlogy -- Experiment Search System -- Data Set -- Subject Domain Based on MeSH Categories -- Search Topics and Tasks -- Participants -- Knowledge Level Elicitation -- Relevance Judgment and Search Performance Measures -- Procedure -- Results -- Evidences of Differences between TK and BK -- Impact of the Two Types of Knowledge on Search Performance -- Discussion and Conclusions -- References -- Community Detection by Local Influence -- Introduction -- Previous Developments in Overlapping Community Detection -- Community Detection by Local Influence -- The Local Influence Score -- The Community Detection Algorithm -- The Community Detection Algorithm -- Complexity -- Evaluation -- Benchmark and Evaluation Metric -- Results -- Conclusion -- References -- Predict Sepsis Level in Intensive Medicine - Data Mining Approach -- Introduction -- Background -- SEPSIS -- Data Mining -- Related Work -- Data-Driven -- Data Mining Models -- Results -- Conclusions and Future Work -- References -- Constructing Conceptual Model for Security Culture in Health Information Systems Security Effectiveness -- Introduction -- Related Works on Information Security Effectiveness -- Security Culture -- Security Education and Training -- Security Communication -- The Conceptual Model -- Research Methodology -- Conclusion and Future Works -- References -- Using Domain-Specific Term Frequenciesto Identify and Classify Health Queries -- Introduction -- Related Work -- Proposed Method for Query Classification -- Health Semantic Structures -- Vocabulary Translation -- CHV Subsets -- Auxiliary Structures -- Combining Inverted Index Entries -- Final Score Calculation -- Classifying Health Queries -- Findings and Discussion -- Conclusions -- References. , Dealing with Constraint-Based Processes: Declare and Supervisory Control Theory -- Introduction -- Declare -- Supervisory Control Theory -- Monolithic Approach -- Local Modular Approach -- Control Architecture -- Running Example -- Implementation in DECLARE -- Implementation Using SCT -- Discussion -- Conclusion -- References -- Adopting Standards in Nursing Health Record - A Case Study in a Portuguese Hospital -- Introduction -- Standards -- What Are They? What Is Their Purpose? -- Nursing Standards -- Research Design and Methodology -- Object of Study -- Investigation Objectives -- Investigation Methodology -- Investigation Question and Assumptions -- Definition of the Medium and the Sample -- Data Collection -- Ethical Considerations -- Discussion and Conclusion -- References -- The Relationship between Portal Quality and Citizens' Acceptance: The Case of the Kuwaiti e-Government -- Introduction -- e-Governments in Kuwait -- e-Government Quality and Acceptance -- Methodology -- Data Analysis and Results -- Conclusions -- References -- Knowledge Management Framework for Six Sigma Performance Level Assessment -- Introduction -- Literature Review -- Concepts and Tools Applied in Knowledge Management Framework -- Concepts and Tools Applied in Data Mart -- Case Study -- Step 1. Knowledge Management Framework Description -- Step 2. DM Structure Development for KM Framework -- Conclusion -- References -- Android, GIS and Web Base Project, Emergency Management System (EMS) Which Overcomes Quick Emergency Response Challenges -- Introduction -- Problem Statement -- Role of GIS -- Reasons to Use Mobile Phones -- Use of Sensors in EMS -- Reasons to Use Web Services -- The Function of GIS in Web Service -- Design and architecture of EMS -- Platform Design -- System Development -- Algorithm -- Flow Chart -- Conclusion -- References. , Pervasive Intelligent Decision Support System - Technology Acceptance in Intensive Care Units.

Note: Intro -- Preface -- Contents -- 1 Dictyostelium discoideum as a Model in Biomedical Research -- Abstract -- 1…Introduction -- 2…What Makes Social Amoebas Different? -- 3…From the Soil to the Laboratory: The Early Times of D. Discoideum Research -- 4…The Advent of Molecular Genetics Propelled D. discoideum into the Post-genomic Era -- 5…A New Frontier in D. discoideum Research: Modeling Human Disease -- 5.1 Pathogen--Host Interactions in D. discoideum -- 5.2 Pathobiology of Cell Motility and Chemotaxis -- 5.3 Autophagy and Protein Aggregation Disorders -- 5.4 The D. dictyostelium Model of Mitochondrial Disease -- 5.5 Molecular Pharmacology in D. dictyostelium -- 6…Concluding Remarks -- Acknowledgments -- References -- 2 Genome Analysis of Social Amoebae -- Abstract -- 1…Genomics -- 2…Nuclear Genomes of Social Amoebae -- 2.1 The Model Organism D. discoideum -- 2.2 Comparative Sequencing of Other Social Amoebae -- 3…Plasmids, rDNA Palindrome, and Mitochondrial Genomes -- 3.1 Plasmids -- 3.2 rDNA Palindromes -- 3.3 Mitochondria -- 4…Regulation of Transcription on a Global Scale -- 5…Curation of Genomes and Databases -- 6…Future Directions of Genomics in Social Amoebae -- References -- 3 Signalling During Dictyostelium Development -- Abstract -- 1…Introduction -- 2…Cell Movement and Signalling to the Cytoskeleton -- 3…Cellular Behaviours During Chemotaxis -- 4…Signalling During Chemotaxis -- 5…Cell--Cell Signalling Controlling Cell Movement During Multicellular Development -- 6…Aggregation -- 7…Mound and Slug Formation -- 8…Differentiation -- Acknowledgments -- References -- 4 The Chemotactic Compass -- Abstract -- 1…Chemotaxis -- 2…Dictyostelium as Model System for Chemotaxis -- 3…cAMP and Folic Acid -- 4…The Dictyostelium cAMP Receptors -- 5…cAR Structure and Localization -- 6…Signaling After Receptor Activation. , 7…Temporal Responses to Chemoattractants Provide Valuable Spatial Information -- 8…The Role of Polarity in Migration -- 9…Dictyostelium Heterotrimeric G Proteins and Functions -- References -- 5 Transcriptional Regulators: Dynamic Drivers of Multicellular Formation, Cell Differentiation and Development -- Abstract -- 1…Introduction -- 2…Entering Development -- 3…Multicellular Assembly -- 4…Culmination and Fruiting Body Formation -- 5…Open Questions and Future Directions -- References -- 6 Non-coding RNAs in Dictyostelium discoideum and Other Dictyostelid Social Amoebae -- Abstract -- 1…Introduction -- 2…lncRNAs as Developmental Regulators -- 3…Medium-Sized ncRNAs -- 3.1 Class I RNAs are Involved in Development and Conserved Throughout Dictyostelia -- 3.2 Spliceosomal RNAs with Unexpected Features -- 3.3 snoRNAs: Modifiers of RNA -- 3.4 Non-coding RNAs with Functions in Protein Delivery and RNA Processing -- 3.5 Medium-Sized ncRNAs with Unknown Functions:Specific to D. discoideum? -- 4…Small RNAs: Important Regulators of Gene Expression -- 4.1 Abundant Small Interfering RNAs Derived from the Transposon DIRS-1 -- 4.2 MicroRNAs in D. discoideum -- 5…Conserved ncRNA Gene Promoter Element? -- 6…Conclusions and Future Perspectives -- Acknowledgments -- References -- 7 Sex in Dictyostelia -- Abstract -- 1…Introduction -- 2…Historical Background -- 3…The Biology of Macrocysts and Macrocyst Formation -- 4…Sexual and Parasexual Genetics -- 5…Evolutionary, Taxonomic and Ecological Considerations -- 6…Outlook -- Acknowledgments -- References -- 8 A Global Overview of Dictyostelid Ecology with Special Emphasis in North American Forest -- Abstract -- 1…Introduction -- 2…Dispersal -- 3…Relative Abundance -- 4…Diversity and Numbers in Tropical and Subtropical Environments -- 5…Optimum Habitat for Dictyostelids -- 6…Dictyostelid Decline. , 7…Ecology of Dictyostelium discoideum -- 8…Ecological Individuality -- 9…Notes on Global Distribution -- 10…Conclusions -- References -- 9 Evolution of Dictyostelid Social Amoebas Inferred from the Use of Molecular Tools -- Abstract -- 1…Introduction -- 2…Morphology Versus Molecular Data -- 3…Diversification of Dictyostelia in the Proterozoic -- 4…Ecology and Biogeography of Protists? -- 5…Concluding Remarks -- Acknowledgments -- References -- 10 The Evolution of the Cellular Slime Molds -- Abstract -- 1…The Great Power of Natural Selection for Dispersal -- 2…The Ability of Slime Molds to Move and Orient to Facilitate Dispersal -- 3…The Paucity of Fruiting Body Shapes -- 4…Evidence for Selection to Specific Environments -- Acknowledgments -- References -- 11 Social Selection in the Cellular Slime Moulds -- Abstract -- 1…Introduction -- 2…Social Selection -- 3…Development of Sociality -- 4…Traits on Which Social Selection can Act -- 5…Stochastic Factors and Genetic or Environmental Differences can Make Pre-aggregation Cells Differ in Their Capacity to Withstand Starvation and Sporulate -- 6…Intercellular Interactions Reinforce Spontaneously Occurring Differences and Lead to Social Selection -- 7…Evolutionary Consequences of Social Selection -- 8…Summing Up -- Acknowledgments -- References -- 12 The Non-dictyostelid Sorocarpic Amoebae -- Abstract -- 1…Introduction -- 2…The History of Sorocarpic Amoeba Research -- 3…Life Cycle -- 4…The Five Groups of Non-dictyostelid Sorocarpic Amoebae -- 4.1 Amoebozoa: Copromyxidae -- 4.2 Excavata: Acrasidae -- 4.3 Opisthokonta: Fonticulaceae -- 4.4 Rhizaria: Guttulinopsidae -- 4.5 Stramenopiles: Sordiplophrys -- 5…Outstanding Questions -- Acknowledgments -- References -- Index.

Note: Cover -- Title -- Table of Contents -- The Legacy of a Great Researcher -- Perspective and Genesis -- Combinatory Logic -- Boolean Algebra -- Logic Calculi and More Enhancements -- Group Theory -- Other Areas of Abstract Algebra -- Introducing Bill McCune -- References -- The Strategy Challenge in SMT Solving -- Introduction -- Caveat Emptor: What This Paper Is and Is Not -- Overview -- Strategy in Mechanized Proof -- What is Strategy? -- Strategy in Automated Theorem Proving over FOL -- Strategy in LCF-Style Interactive Proof Assistants -- Foundations for Big-Step Strategies -- Parametric Reasoning Engines as Tacticals -- Strategies in Action -- Z3 QF_LIA Strategy -- Calculemus RAHD Strategies -- Conclusion -- References -- Simple and Efficient Clause Subsumptionwith Feature Vector Indexing -- Introduction -- Preliminaries -- Subsumption -- Subsumption Variants -- Saturation Procedures and Clause Set Subsumption -- Feature Vector Indexing -- Subsumption-Compatible Clause Features -- Clause Feature Vectors and Candidate Sets -- Index Data Structure -- Forward Subsumption -- Backward Subsumption -- Optimizing the Index Data Structure -- Implementation Notes -- Experimental Results -- Prover Instrumentation and Configuration -- Feature Selection -- Feature Vector Optimization -- Basic Performance -- Profiling and Time Behavior -- Performance in Automatic Mode -- Future Work -- Conclusion -- References -- Superposition for Bounded Domains -- Introduction -- Getting Started -- A Calculus for T-unsatisfiability -- Calculus Rules -- Redundancy in SB and in S -- Application to Unit Rewriting -- Obtaining a Decision Procedure -- Calculus Rules -- Soundness and Refutational Completeness -- Termination by Loop Detection -- Termination by Rewriting -- Extensions -- Combinations with Unbounded First-Order Theories -- Three Application Scenarios. , Combination with Theories -- Vectors over Finite Domains -- Proof Obligations from ISABELLE -- Conclusion and Future Work -- References -- MACE4 and SEM: A Comparison of Finite Model Generators -- Introduction -- Model Generation: Basic Concepts and Notations -- Two Small Examples -- Input of Mace4 and SEM -- Preprocessing -- Basic Search Algorithm in Mace4 and SEM -- A Backtracking Search Procedure -- Avoiding Search for Isomorphic Models -- Selecting Cells -- Constraint Propagation -- Simplification Rules -- Inference Rules -- Empirical Evaluation -- Algebra and Logic -- Quasigroup Problems -- Experimental Results -- A Challenging Latin Square Problem -- Basic Concepts -- Specification of (3,2,1)-ICODLS(11,3) -- Construction of (3,2,1)-ICODLS(11,3) -- Conclusion and Future Works -- References -- Group Embedding of the Projective Plane PG(2, 3) -- Bill McCune -- Finite Projective Planes as Groups -- The Procedure for Group Embedding of PG(2,3). -- An Example of an Impossibility Proof -- Prover9 Steps -- References -- A Geometric Procedure with Prover9 -- In Memory of Bill McCune -- A First-Order Property for Cubic Curves -- Implementing gL in Prover9 -- Group Law on Non-singular Cubic Curves -- Conclusion -- References -- Loops with Abelian Inner Mapping Groups: An Application of Automated Deduction -- Introduction -- The Main Conjecture and the Project -- The Strategy -- LC Loops -- Further Remarks -- References -- (Dual) Hoops Have Unique Halving -- Introduction -- The Logics -- Algebraic Semantics -- Automated Proofs and Counterexamples -- Subsequent Work -- Final Remarks -- References -- Gibbard's Collapse Theorem for the Indicative Conditional: An Axiomatic Approach -- Background: Gibbard's (Informal) Argument -- Axiomatization of the Gibbardian Collapse Phenomenon -- Concluding Remarks -- Appendix: Proofs of Theorems. , Proofs of the Independence of Our Axioms (1)-(8) -- Proof of Our (Intuitionistic) Collapse Theorem -- Counterexample to Peirce's Law for and -- References -- Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants -- Introduction -- Related Work -- On the Quality of Invariants Generated Using Quantifier Elimination -- Octagonal Invariants -- Overview -- Program Analysis Using Octagonal Invariants -- Trivially Redundant and Implicit Conditions -- Localized Quantifier Elimination -- Geometric View of Quantifier Elimination -- Reversal of the Signs of Both Variables -- The Signs of Both Variables Remain Invariant -- The Sign of Exactly One Variable Is Reversed -- The Effects of Computing the Closure of the Tests and Choosing Different Table Entries -- Programs with Multiple Loops -- Strongest Invariants and Complexity -- Invariant Generation with Max-plus Polyhedra -- Invariant Generation -- Concluding Remarks and Future Work -- References -- Toward a Procedure for Data Mining Proofs -- Introduction -- Proof Sketches -- Applications of Mutual Information -- Mutual Information -- Applications of Mutual Information -- Experimental Results -- Boolean Algebra -- Field Theory -- Group Theory -- Conclusion -- References -- Theorem Proving in Large Formal Mathematics as an Emerging AI Field -- OTTER and QED -- Why Link Large Formal Mathematics with AI/ATP Methods? -- Why Mizar? -- MPTP: Translating Mizar for Automated Reasoning Tools -- Experiments and Projects Based on the MPTP -- Re-proving Experiments -- Finding New Proofs and the AI Aspects -- ATP-Based Explanation, Presentation, and Cross-verification of Mizar Proofs -- Use of MPTP for ATP Challenges and Competitions -- Development of Larger AI Metasystems Like MaLARea and MaLeCoP on MPTP Data -- Future QED-Like Directions -- References -- Author Index.

Note: Intro -- Preface -- Organization -- Table of Contents -- A Pre-processing Aware RINS Based MIP Heuristic -- 1 Introduction -- 2 Literature Review -- 3 The pRINS MIP Heuristic -- 4 Characterization of Instances -- 5 Experiments and Results -- 6 FinalRemarks -- References -- A Hybrid Simulated Annealing Algorithm for Location of Cross-Docking Centers in a Supply Chain -- 1 Introduction -- 2 Problem Description and Formulation -- 2.1 Proposed Model -- 3 Proposed Hybrid Meta-heuristic Algorithm -- 4 Computational Results -- 5 Conclusion -- References -- Intensification/Diversification in Decomposition Guided VNS -- 1 Introduction -- 2 Context and Definitions -- 2.1 Cost Functions Network -- 2.2 Tree Decomposition -- 2.3 Decomposition Guided VNS (DGVNS) -- 3 Strategies for Intensification/Diversification in -- 3.1 Intensification versus Diversification -- 3.2 DGVNS-1: Move Systematically to the Next Cluster -- 3.3 DGVNS-2: Move to the Next Cluster If No Improvement Is Made -- 3.4 DGVNS-3: Move to the Next Cluster after Each Improvement -- 4 Benchmark Problems -- 5 Experiments -- 5.1 Experimental Protocol -- 5.2 Comparing the Three Strategies -- 5.3 Comparing with Other Approaches -- 6 Conclusions -- References -- A Hybridized Particle Swarm Optimization with Expanding Neighborhood Topology for the Feature Selection Problem -- 1 Introduction -- 2 Feature Selection Problem -- 3 Particle Swarm Optimization with Expanding Neighborhood Topology Algorithm -- 3.1 General Description -- 4 Computational Results -- 5 Conclusions -- References -- Interleaving Constraint Propagation: An Efficient Cooperative Search with Branch and Bound -- 1 Introduction -- 2 Cooperative Search Framework -- 2.1 The SOLVE Component -- 2.2 The OBSERVATION Component -- 2.3 The ANALYSE Component -- 2.4 The UPDATE Component -- 3 B& -- B + Constraint Propagation Solver. , 3.1 Basic Hybridization -- 3.2 Hybridization Based on Propagation Rate -- 4 Conclusion -- References -- Automatic Tuning of GRASP with Evolutionary Path-Relinking -- 1 Introduction -- 2 GRASP with Evolutionary Path-Relinking -- 3 Automatic Tuning Using a BRKGA -- 3.1 Encoding and Decoding -- 4 GRASP+evPR for Three Optimization Problems -- 4.1 Set Covering -- 4.2 Maximum Cut -- 4.3 Node Capacitated Graph Partitioning -- 5 Experimental Results -- 5.1 Instances -- 5.2 The Experiments -- 6 Concluding Remarks -- References -- Combining Genetic Algorithm and Simulated Annealing Methods for Reconstructing HV-Convex Binary Matrices -- 1 Introduction -- 2 Preliminaries -- 3 HV-ConvexBinaryMatrix -- 3.1 Definitions -- 3.2 Integer Programming Formulation -- 3.3 Bounds -- 4 Simulated Annealing -- 4.1 Overview -- 4.2 Simulated Annealing for RBM(H,V) -- 5 Genetic Algorithm -- 5.1 Overview -- 5.2 Genetic Algorithm for RBM(H,V) -- 6 Combining GA and SA Algorithm (GASA) for -- 6.1 GASA Algorithm -- 7 Computational Results -- 7.1 Choice of the Parameters -- 7.2 Results -- 8 Conclusion -- References -- Experimental Analysis of Pheromone-Based Heuristic Column Generation Using irace -- 1 Introduction -- 2 Vehicle Routing Problems with Black Box Feasibility -- 2.1 The Capacitated Vehicle Routing Problem and Black-Box Feasibility -- 2.2 Applications of the VRPBB -- 3 Pheromone-Based Heuristic Column Generation for the VRPBB -- 3.1 Reformulation as Set Partitioning Problem -- 3.2 Pheromone-Based Heuristic Column Generation (ACO-HCG) -- 4 Experimental Setup -- 5 Experimental Results -- 5.1 Manual vs. Automatic Parameter Configurations -- 5.2 Experimental Analysis of the ACO-HCG Parameters -- 6 Conclusion -- References -- A New Hybrid Metaheuristic - Combining Stochastic Tunneling and Energy Landscape Paving -- 1 Introduction -- 1.1 Previous Work. , 1.2 Our Contribution: Synergistically Combining STUN and ELP -- 2 A Combined Algorithm -- 3 A Test Instance -- 4 Results -- 4.1 Performance Benchmarking - Quality of Solutions -- 4.2 Statistical Properties of Search Dynamics -- 4.3 Sensitivity Analysis to -- Choices -- 5 Conclusions -- References -- Workgroups Diversity Maximization: A Metaheuristic Approach -- 1 Introduction -- 2 A Mathematical Model for the Workgroup Diversity Problem -- 3 A Pool-Based Metaheuristic Algorithm -- 4 Computational Results and Statistical Analysis -- 5 Conclusions and Future Work -- References -- Balancing Bicycle Sharing Systems: Improving a VNS by Efficiently Determining Optimal Loading Operations -- 1 Introduction -- 2 Problem Definition -- 3 Variable Neighborhood Search for BBSS -- 3.1 VND Neighborhood Structures -- 3.2 VNS Neighborhoods Structures -- 4 Maximum Flow Based Method for the General Case -- 5 Combined Approach -- 6 Computational Results -- 7 Conclusions and Future Work -- References -- Automatic Design of Hybrid Stochastic Local Search Algorithms -- 1 Introduction -- 2 Generalized Local Search Structure -- 3 Implementation -- 3.1 A Practical Implementation of the GLS Structure -- 3.2 A Grammar Description of the GLS Structure -- 3.3 Automatic Generation of Hybrid LS Metaheuristics -- 4 Experimental Setup -- 4.1 The PFSP-WT -- 4.2 Local Search Components for the PFSP-WT -- 4.3 Experimental Protocol -- 5 Experimental Results -- 6 Conclusion -- References -- GRASP and Variable Neighborhood Search for the Virtual Network Mapping Problem -- 1 Introduction -- 2 The Virtual Network Mapping Problem -- 3 Background and Related Work -- 4 GRASP -- 5 VNS -- 6 Results -- 6.1 GRASP -- 6.2 VNS -- 6.3 Comparison -- 7 Conclusions -- References -- Hybrid Metaheuristics for the Far From Most String Problem -- 1 The Far From Most String Problem (FFMSP). , 2 Hybrid Metaheuristics -- 2.1 A Pure GRASP -- 2.2 A Pure VNS -- 2.3 Path-Relinking -- 2.4 Hybrid GRASP with Path-Relinking -- 2.5 Hybrid GRASP with VNS -- 2.6 Hybrid VNS with Path-Relinking -- 2.7 Hybrid GRASP with VNS and Path-Relinking -- 3 Experimental Results -- 4 Concluding Remarks and Future Work -- References -- On Missing Data Hybridizations for Dimensionality Reduction -- 1 Introduction -- 2 Unsupervised Nearest Neighbors -- 2.1 Unsupervised Regression -- 2.2 Iterative Unsupervised Regression -- 2.3 Latent Sorting -- 3 Missing Data -- 3.1 Repair-and-Embed -- 3.2 Embed-and-Repair -- 4 Experimental Comparison of Missing Data Methods -- 5 Conclusions -- References -- A Hybrid ACO+CP for Balancing Bicycle Sharing Systems -- 1 Introduction -- 2 Related Work -- 3 A Constraint Model for BBSP -- 3.1 Variables -- 3.2 Constraints -- 4 AnACO+CPHybrid -- 4.1 ACO+CP for BBSP -- 5 Experimental Analysis -- 6 Conclusions and Future Work -- References -- Author Index.

Note: Preface -- Contents -- Acronyms -- 1 Introduction and Background -- 1.1 Climate Change -- 1.1.1 Weather and Climate -- 1.1.2 A Brief History of Climatic Research -- 1.1.3 The Physical Mechanisms of Anthropogenic Global Warming -- 1.1.4 Emission Scenarios -- 1.1.5 Impacts: The Ocean Wave Climate -- 1.1.6 Ocean Waves and Maritime Safety -- 1.2 Stochastic Modeling of Environmental Processes -- 1.2.1 Probabilistics Versus Deterministics -- 1.2.2 Bayesian Hierarchical Space-Time Models -- 1.2.3 Waves as Stochastic Processes -- 1.3 Data -- 1.4 Some Identified Areas for Further Research -- References -- 2 Literature Survey on Stochastic Wave Models -- 2.1 Wave Data and Data Sources -- 2.2 Review of Statistical Models for Extreme Waves -- 2.2.1 Short-Term Stochastic Wave Models -- 2.2.2 Stationary Models -- 2.2.3 Non-Stationary Models -- 2.3 Relevant Statistical Models from Other Areas of Application -- 2.3.1 Bayesian Hierarchical Space-Time Models -- 2.3.2 Continuous Space Models -- 2.3.3 Process Convolution Models -- 2.3.4 Non-Stationary Covariance Models -- 2.3.5 Coregionalization Models -- 2.3.6 Generalized Extreme Value Models -- 2.3.7 Optimality Models -- 2.3.8 Bayesian Maximum Entropy Models -- 2.3.9 Stochastic Diffusion Models -- 2.3.10 Regional Frequency Analysis -- 2.4 Selecting a Modeling Approach -- 2.5 Wave Climate Projections -- 2.5.1 Climate Change -- 2.5.2 Current Trends in the Wave Climate -- 2.5.3 Projections of Future Trends in the Wave Climate -- 2.6 Summary and Conclusions -- References -- 3 A Bayesian Hierarchical Space-Time Model for Significant Wave Height -- 3.1 Data and Area to be Considered -- 3.1.1 Data Description -- 3.1.2 Area Description -- 3.1.3 Initial Data Analysis -- 3.2 Model Description -- 3.2.1 Main Model -- 3.2.2 Model Alternatives -- 3.2.3 Prior Distributions on the Model Parameters. , 3.3 Model Comparison and Selection -- 3.3.1 Sum of Squares of the Residuals -- 3.3.2 Loss Functions Based on Predictive Power -- 3.4 Implementation and Simulations -- 3.5 Results and Predictions -- 3.5.1 Results for Monthly Data -- 3.5.2 Results for Daily Data -- 3.5.3 Results for Monthly Maximum Data -- 3.5.4 Model Comparison and Selection -- 3.5.5 Future Projections -- 3.5.6 General Comments -- 3.6 Discussion -- 3.7 Summary and Conclusions -- References -- 4 Including a Log-Transform of the Data -- 4.1 Introduction and Motivation -- 4.2 Re-Transformation Bias Correction -- 4.3 Revised Model Description -- 4.3.1 Prior Distributions -- 4.3.2 Loss Functions for Model Comparison -- 4.4 Simulations and Results -- 4.4.1 Results for Monthly Data -- 4.4.2 Results for Daily Data -- 4.4.3 Results for Monthly Maximum Data -- 4.4.4 Simulations on 6-Hourly Data -- 4.4.5 Model Comparison and Selection -- 4.4.6 Future Projections -- 4.5 Discussion -- 4.5.1 Semi-Annual Seasonal Component -- 4.6 Summary and Conclusions -- References -- 5 CO2 Regression Component for Future Projections -- 5.1 Introduction and Background -- 5.2 Data Description -- 5.2.1 Historic Data -- 5.2.2 Future Projections -- 5.3 Model Extension -- 5.3.1 Model Alternatives -- 5.3.2 Critical Model Assumptions -- 5.3.3 Prior Distributions -- 5.4 Results and Predictions -- 5.4.1 MCMC Simulations -- 5.4.2 Simulation Results -- 5.4.3 Results with a Semi-Annual Component -- 5.4.4 Results for Control Runs -- 5.5 Model Comparison and Selection -- 5.6 Discussion -- 5.7 Summary and Conclusion -- References -- 6 Bayesian Hierarchical Modeling of the Ocean Windiness -- 6.1 Data Description and Area of Investigation -- 6.1.1 Wind Data -- 6.1.2 Area Description -- 6.2 The Stochastic Model -- 6.2.1 Main Model Specification -- 6.2.2 Alternative Models -- 6.2.3 MCMC Simulations -- 6.3 Results. , 6.3.1 Results From the Main Model -- 6.3.2 Results From the Model with No Trend -- 6.3.3 Results From the Log-Transformed Model -- 6.3.4 Results Pertaining to Another Ocean Area -- 6.4 Discussion -- 6.5 Summary and Conclusions -- References -- 7 Application: Impacts on Ship Structural Loads -- 7.1 Introduction and Background -- 7.2 Probabilistic Structural Design -- 7.2.1 First Order Reliability Method (FORM) -- 7.2.2 Long-Term Response Analysis -- 7.3 Potential Impact of Climate Change on Ship Structural Loads and Responses -- 7.3.1 Joint Model for Significant Wave Height and Wave Period -- 7.3.2 Environmental Contours -- 7.3.3 Illustrative Example: Load Assessment for an Oil Tanker -- 7.4 Summary and Conclusions -- References -- 8 Case Study: Modeling the Effect of Climate Change on the World's Oceans -- 8.1 Introduction -- 8.2 Simulation Results for the Various Ocean Areas -- 8.2.1 North Atlantic Ocean -- 8.2.2 North East Pacific: Western USA/Canada -- 8.2.3 Gulf of Mexico -- 8.2.4 South Atlantic Ocean: West Africa -- 8.2.5 North West Pacific Ocean: Japan -- 8.2.6 Indian Ocean -- 8.2.7 South Pacific Ocean: Chile -- 8.2.8 Mid Atlantic Ocean -- 8.2.9 Tasmanian Sea: Eastern Australia -- 8.2.10 Mediterranean Sea -- 8.2.11 Equatorial Pacific -- 8.2.12 Western Australia -- 8.3 Prediction Losses -- 8.4 Discussion -- 8.5 Conclusion -- References -- 9 Summary and Conclusions -- 9.1 Open Issues and Suggestions for Further Work -- A Markov Chain Monte Carlo Methods -- A.1 Standard Monte Carlo Integration -- A.1.1 Inversion Sampling -- A.1.2 Accept--Reject Simulation -- A.1.3 Importance Sampling -- A.2 Monte Carlo Variance -- A.3 Markov Chain Monte Carlo -- A.3.1 Essential Markov Chain Theory -- A.4 The Metropolis-Hastings Algorithm -- A.4.1 Independent Metropolis-Hastings Algorithms -- A.4.2 Random Walk Metropolis-Hastings Algorithms. , A.5 The Slice Sampler -- A.5.1 2D Slice Sampler -- A.5.2 The General Slice Sampler -- A.6 Gibbs Sampling -- A.6.1 The Two-Stage Gibbs Sampler -- A.6.2 Multi-Stage Gibbs Sampler -- Reference -- B Extreme Value Modeling -- B.1 Generalized Extreme Value Distribution -- B.2 Three Families of Extreme Value Distributions -- B.3 The Generalized Pareto Distribution -- B.3.1 The Poisson-GPD Model -- B.4 Extreme Values of Dependent Sequences -- B.4.1 Maxima of Stationary Dependent Sequences -- B.5 Non-Stationary Generalized Extreme Value Model -- Reference -- C Markov Random Fields -- C.1 The Hammersley-Clifford Theorem -- C.2 Auto-Models -- C.3 Inference in Markov Random Fields -- C.3.1 Coding Methods -- C.3.2 Pseudo-Likelihood -- C.3.3 Maximum Likelihood in Gaussian Markov Random Fields -- C.3.4 General Maximum Likelihood (simulated ML) -- C.3.5 Bayesian Methods -- D Derivation of the Full Conditionals of the Bayesian Hierarchical Space-Time Model for Significant Wave Height -- D.1 Conditional Distribution for H(t) -- D.2 Conditional Distribution for μ -- D.3 Conditional Distribution for θ(t) -- D.3.1 Pt -- D.3.2 Ptt -- D.3.3 p0 -- D.4 Conditional Distribution for μ0 -- D.5 Conditional Distribution for b0, bN, bE, bS, and bW -- D.6 Conditional Distribution for aφ and aλ -- D.7 Conditional Distribution for Mt -- D.8 Conditional Distribution for c, d, γ, and η -- D.9 Conditional Distribution for σ2Z -- D.10 Conditional Distribution for σ2μ -- D.11 Conditional Distribution for σθ2 -- D.12 Conditional Distribution for σm2 -- E Sampling from a Multi-normal Distribution -- E.1 Sampling from a Bivariate Normal Distribution -- Ocean Engineering & -- Oceanography -- Foreword -- Foreword -- Preface -- Acknowledgments -- Contents -- Acronyms.

Note: Intro -- Series Editors -- Advisory Board -- Preface -- Acknowledgments -- Contents -- 1 Introduction: Independent Strain and Transport Motions -- 1.1…Introduction -- 1.2…Strain and Transport Motions -- References -- 2 Asymmetric Continuum: Basic Motions and Equations -- 2.1…Introduction -- 2.2…Solids: Strain Fields and Molecular Transport -- 2.3…Fluids: Molecular Strains and Transport -- 3 Transport and Float Transport Motions -- 3.1…Introduction -- 3.2…Coriolis Effect -- 3.3…Motions in Solids -- 3.4…Motions in Fluids -- 3.5…Glaciers -- 4 Vortices and Molecular Fracture Transport -- 4.1…Introduction -- 4.2…Vortices and Molecular Fracture Transport -- 5 Defect Densities -- 5.1…Introduction -- 5.2…Defect Densities -- References -- 6 Structural and Fracture Anisotropy -- 6.1…Introduction -- 6.2…Structural and Fracture Anisotropy -- References -- 7 Induced Strains -- 7.1…Introduction -- 7.2…Induced Strains -- References -- 8 Thermodynamic Relations -- 8.1…Introduction -- 8.2…Thermodynamic Functions -- 8.3…Thermodynamics of Point Defects in Solids -- The cB Omega Model -- 8.4…Linear Defects -- 8.5…Superlattice and Shear Band Model -- References -- 9 Mutual Interactions: Electric/Magnetic Fields and Strains -- 9.1…Introduction -- 9.2…Earthquake Prediction: Seismic Electric Signals and Natural Time Analysis -- 9.2.1 Proposal of a New Time Domain -- 9.2.2 Strains and Electric/Magnetic Fields -- References -- 10 Quantum Analogies -- 10.1…Introduction -- 10.2…Quantum Analogies -- References -- 11 Extreme Processes -- 11.1…Introduction -- 11.2…Extreme Processes -- References -- 12 Release-Rebound Processes and Motions -- 12.1…Introduction -- 12.2…Release-Rebound Processes and Motions -- References.

Note: Intro -- Preface -- Organization -- Table of Contents -- One Logic to Use Them All -- 1 Introduction -- 2 A Polymorphic First-Order Logic -- 2.1 Syntax -- 2.2 Type Checking -- 2.3 Semantics -- 2.4 Implementation -- 3 Targeting Multiple Provers -- 3.1 Tasks and Transformations -- 3.2 Drivers -- 3.3 Proof Sessions -- 3.4 Examples -- 4 Experimental Results -- 5 Related Work -- 6 Conclusion and Perspectives -- References -- The Tree Width of Separation Logic with Recursive Definitions -- 1 Introduction -- 2 Preliminaries -- 2.1 Syntax and Semantics of Monadic Second Order Logic -- 2.2 Syntax and Semantics of Separation Logic -- 3 Decidability of Satisfiability and Entailment in SLRD -- 3.1 A Decidable Subset of SLRD -- 4 FromSLRDbtw to MSO -- 4.1 Converting Basic SL Formulae to MSO -- 4.2 States and Backbones -- 4.3 Inner Edges -- 4.4 Double Allocation -- 4.5 Handling Parameters -- 4.6 Translating Top Level SLRDbtw Formulae to MSO -- 5 Conclusions and Future Work -- References -- Hierarchic Superposition with Weak Abstraction -- 1 Introduction -- 2 The Tableau Calculus -- 3 TheSibyl Prover -- 4 Concluding Remarks -- References -- Completeness and Decidability Results for First-Order Clauses with Indices -- 1 Introduction -- 1.1 Related Work -- 2 Preliminaries -- 3 A Superposition Calculus for Indexed Clauses -- 4 Loop Detection -- 5 Completeness -- 6 Satisfiability Detection -- 7 Complete Classes of Indexed Formulæ -- 8 Conclusion -- References -- A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies -- 1 Introduction -- 2 The Tableau Calculus -- 3 TheSibyl Prover -- 4 Concluding Remarks -- References -- Tractable Inference Systems: An Extension with a Deducibility Predicate -- 1 Introduction -- 1.1 The Application Context -- 1.2 Difficulties -- 1.3 Overview of the Results and Proofs -- 2 Formal Setting. , 3 Tractability of Deducibility Axioms -- 3.1 Adding Equality -- 3.2 Adding a Function Axiom -- 4 More Clauses Using the Deducibility Predicate -- 4.1 Adding Other Predicate Symbols -- 4.2 Adding Equality -- 5 The General Case -- 6 Conclusion -- References -- Computing Tiny Clause Normal Forms -- 1 Introduction -- 2 Background -- 3 Generalized Formula Renaming -- 3.1 A Generalized Renaming Algorithm -- 4 Experiments -- 4.1 Comparing the Size of CNF -- 4.2 Comparing Theorem Proving Time -- 5 Conclusion -- References -- System Description: E-KRHyper 1.4 -- 1 Introduction -- 2 General Overview of E-KRHyper -- 3 Extensions in Version 1.4 -- 3.1 Support for the Unique Name Assumption -- 3.2 Support for SHIQ -- 4 Related Systems and Performance Evaluation -- 4.1 Unique Name Assumption -- 4.2 Description Logic -- 5 Conclusion -- References -- Analysing Vote Counting Algorithms via Logic -- 1 Introduction -- 2 The Single Transferable Vote Scheme -- 3 Semantic Criteria for Judging Voting Schemes -- 4 The System for Analysing Vote Counting Algorithms -- 4.1 Vote Counting Algorithms as Linear-Logic Programs -- 4.2 Bounded Model Checker -- 5 Case Study: CADE-STV -- 6 Conclusion -- References -- Automated Reasoning, Fast and Slow -- 1 A Critique of Deductive Inference -- 2 Probabilistic Inference -- 3 Cueology -- 4 Discussion -- 5 Conclusions -- References -- Foundational Proof Certificates in First-Order Logic -- 1 Introduction -- 2 Proof Theory Architecture -- 3 Software Architecture -- 3.1 Programming Language Support -- 3.2 Clerks and Experts -- 3.3 Defining a Proof Certificate Definition -- 4 Some Certificate Definitions for Classical Logic -- 4.1 A Decision Procedure -- 4.2 Matings -- 4.3 Resolution Refutations -- 4.4 Capturing General Computation within Proofs -- 5 Adequacy of Encoding -- 6 The More General Kernel -- 7 Related and Future Work. , 8 Conclusion -- References -- Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals -- 1 Overview and Related Work -- 2 Theoretical Background -- 3 Implementing Field Extensions -- 3.1 Transcendental Extensions -- 3.2 Infinitesimal Extensions -- 3.3 Algebraic Extensions -- 4 Examples -- 5 Conclusion -- References -- A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition -- 1 Introduction -- 2 Preliminaries -- 2.1 Real Arithmetic -- 2.2 Satisfiability-Modulo-Theories (SMT) Solving -- 3 The SMT Solver iSAT -- 4 Cylindrical Algebraic Decomposition (CAD) -- 4.1 Projection Phase -- 4.2 Construction Phase -- 5 iSAT Adaption -- 6 CAD Adaption -- 7 Experimental Results -- 8 Outlook -- References -- dReal: An SMT Solver for Nonlinear Theories over the Reals -- 1 Introduction -- 2 Usage -- 2.1 Input Format -- 2.2 Command Line Options -- 3 Design -- 3.1 The δ-Decision Problem -- 3.2 DPLL(ICP) -- 4 Results -- References -- Solving Difference Constraints over Modular Arithmetic -- 1 Introduction -- 2 Deciding Difference Logic -- 3 Wrapped Difference Constraints -- 3.1 Interval Sets -- 3.2 Wrapped-Interval Approximation -- 3.3 Combining Wrapped Difference with Relative Order -- 3.4 NP-Completeness of Wrapped Difference Constraints -- 3.5 SMT Encodings: Two Complete Decision Procedures -- 3.6 An Incomplete Decision Procedure -- 4 Experimental Evaluation -- 5 Conclusion -- References -- Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis -- 1 Introduction -- 2 Preliminaries -- 3 Asymmetric Unification -- 4 An Asymmetric Unification Algorithm for the Theory of Exclusive OR with Uninterpreted Function Symbols -- 5 Decidability of Asymmetric Unification -- 6 Experiments with Unification Problems Arising in Protocol Analysis -- 7 Conclusions and Future Work -- References. , Hierarchical Combination -- 1 Introduction -- 2 Preliminaries -- 3 Combination Procedure -- 3.1 Restrictions -- 3.2 Variable Identification -- 3.3 Termination, Soundness and Completeness -- 4 A Class of Hierarchically Combinable Theories -- 4.1 Satisfying Restriction 1 -- 4.2 Satisfying Restriction 2 -- 4.3 Satisfying Restriction 3 -- 4.4 Unifiability of Partial Solved Forms -- 4.5 Inner Constructor Definitions and Undecidable Results -- 5 Conclusion and Perspective -- References -- PRocH: Proof Reconstruction for HOL Light -- 1 Introduction, Motivation, and Related Work -- 2 Using Existing Approaches on HOL Light Problems -- 3 PRocH System Description -- 3.1 Translation to FOL and Producing FOL Proofs -- 3.2 Reconstructing Terms and Formulas -- 3.3 Replaying ATP Proofs in HOL Light -- 4 Evaluation -- 5 Conclusion and Future Work -- References -- An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description -- 1 Introduction -- 1.1 A Terse Overview of the Basic Algorithm -- 1.2 Basic Implementation Details -- 2 Optimisations -- 3 Results -- 4 Conclusion, Further Work and Acknowledgements -- References -- Towards Modularly Comparing Programs Using Automated Theorem Provers -- 1 Introduction -- 2 Background -- 3 Mutual Summaries and Relative Termination -- 3.1 Mutual Summaries -- 3.2 Relative Termination -- 3.3 Modular Checking -- 3.4 Proof Sketch -- 3.5 Encoding in Boogie -- 4 Applications -- 4.1 Loops and Unstructured Control -- 4.2 Intraprocedural Translation Validation -- 4.3 Interprocedural Transformations -- 5 Related Work -- 6 Conclusion -- References -- Reuse in Software Verification by Abstract Method Calls -- 1 Introduction -- 2 Verification Framework -- 3 Delta-Oriented Reuse of Programs and Contracts -- 3.1 Program Deltas -- 3.2 Contract Deltas -- 3.3 Verification of Deltas -- 4 Abstract Method Calls. , 5 Application Scenarios -- 5.1 Abstract Verification -- 5.2 Liskov for Free -- 5.3 Experiments -- 5.4 Program Evolution -- 6 Related Work -- 7 Conclusion -- References -- Dynamic Logic with Trace Semantics -- 1 Introduction -- 2 SyntaxofDTL -- 3 SemanticsofDTL -- 4 A Sequent Calculus for DTL -- 4.1 Classical Logic and Update Rules -- 4.2 Simplification and Normalization Rules -- 4.3 Rules for Temporal Operators -- 4.4 Program Rules -- 4.5 Rules for Data Structures -- 5 Soundness and Completeness -- 6 Conclusions and Further Directions -- References -- Temporalizing Ontology-Based Data Access -- 1 Introduction -- 2 Preliminaries -- 3 The Entailment Problem -- 4 Data Complexity for the Case of Rigid Concepts -- 5 Combined Complexity for the Case of Rigid Concepts -- 6 Conclusions -- References -- Verifying Refutations with Extended Resolution -- 1 Introduction -- 2 Preliminaries -- 2.1 Conjunctive Normal Form -- 2.2 Resolution and Extended Resolution -- 2.3 Boolean Constraint Propagation -- 3 Verification Using the RAT Redundancy Property -- 4 Extended Resolution in Practice -- 4.1 Manually-Constructed Proofs -- 4.2 Extended Learning -- 4.3 Bounded Variable Addition -- 5 Existing Proof Formats -- 5.1 Resolution Proofs -- 5.2 Clausal Proofs -- 6 TheRAT Proof Format -- 7 Implementation -- 8 Evaluation -- 8.1 Manually-Constructed Proofs -- 8.2 Extended Learning -- 8.3 Bounded Variable Addition -- 9 Conclusions -- References -- Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems -- 1 Introduction -- 2 Preliminaries -- 3 Deductive Verification and Synthesis -- 3.1 Parametric Linear Hybrid Automata -- 3.2 Parametric Hybrid Automata -- 3.3 Interconnected Families of Hybrid Automata -- 4 Generating Criticality Functions -- 5 Conclusions -- References. , Quantifier Instantiation Techniques for Finite Model Finding in SMT.

Note: Intro -- Contents -- Preface -- List of Publications of Professor Marco Antonio Chaer Nascimento -- Some recent developments in photoelectrochemical water splitting using nanostructured TiO2: a short review -- Abstract -- Keywords -- Abbreviations -- 1 Introduction -- 2 Mechanistic studies -- 3 Titania nanotubes -- 3.1 Properties -- 3.2 Fabrication -- 3.3 Performance in water splitting -- 4 Composite nanotubes -- 5 Plasmonic effects in solar water splitting -- 6 Conclusions -- Acknowledgments -- References -- Role of step sites on water dissociation on stoichiometric ceria surfaces -- Abstract -- Keywords -- 1 Introduction -- 2 Computational details -- 3 Results and discussion -- 3.1 Water molecular adsorption on ceria surfaces -- 3.2 Water dissociation on ceria surfaces -- 4 Conclusions -- Acknowledgments -- References -- Proton exchange reactions of C2-C4 alkanes sorbed in ZSM-5 zeolite -- Abstract -- Keywords -- 1 Introduction -- 2 Computational details -- 2.1 Models of ZSM-5 and optimizations -- 2.2 Adsorption energy and reaction barrier -- 2.3 Complete basis set (CBS) extrapolation -- 3 Results and discussions -- 3.1 Transition-state structures -- 3.2 Adsorption energy -- 3.3 Proton exchange barrier -- 3.3.1 Cluster-size dependency -- 3.3.2 Basis set dependency -- 3.3.3 Effect of the level of electron correlation -- 3.3.4 Zero-point-energy correction -- 3.3.5 Apparent reaction barriers -- 3.4 Regioselectivity -- 4 Conclusion -- Acknowledgments -- References -- Effects of mutations on the absorption spectra of copper proteins:a QM/MM study -- Abstract -- Keywords -- 1 Introduction -- 2 Computational details and strategy -- 2.1 Computational strategy -- 2.2 Electrostatic polarization of the MM part -- 2.3 Natural transition orbitals -- 3 Results and discussion -- 3.1 Structural parameters. , 3.2 Ground state electronic structure and ESR parameters -- 3.3 Native protein UV/VIS and CD spectra -- 3.4 Plastocyanin mutations -- 4 Conclusions -- Acknowledgments -- References -- Structure and electronic properties of hydrated mesityl oxide: a sequential quantum mechanics/molecular mechanics approach -- Abstract -- Keywords -- 1 Introduction -- 2 Computational methods and details -- 3 Results -- 3.1 Gas-phase properties of mesityl oxide -- 3.2 Properties of the mesityl oxide-water solution -- 3.2.1 Polarization effects of water on hydrated mesityl oxide -- 3.2.2 Structure and hydrogen bonding in the mesityl oxide-water solution -- 3.2.3 Gibbs free energy and conformational change of mesityl oxide in water -- 3.2.4 Absorption spectrum of mesityl oxide in water -- 4 Conclusions -- Acknowledgments -- References -- Density functional and chemical model study of the competition between methyl and hydrogen scission of propane and b-scission of the propyl radical -- Abstract -- Keywords -- 1 Introduction -- 2 Methods -- 3 Results and discussion -- 3.1 Initial steps -- 3.2 Propyl radicals -- 3.3 b-scission reaction -- 3.4 Chain initiation reactions -- 3.5 Chain propagation reactions -- 3.6 Termination reactions -- 4 Discussion -- 5 Conclusions -- Acknowledgments -- References -- CompASM: an Amber-VMD alanine scanning mutagenesis plug-in -- Abstract -- Keywords -- 1 Introduction -- 2 Methodology -- 3 Software description -- 4 Results -- 5 Conclusions -- Acknowledgments -- References -- Spectrum simulation and decomposition with nuclear ensemble: formal derivation and application to benzene, furan and 2-phenylfuran -- Abstract -- Keywords -- 1 Introduction -- 2 Derivation of the nuclear-ensemble method -- 2.1 Absorption cross section -- 2.2 Overlap function: approximation 1 -- 2.3 Overlap function: approximation 2 -- 2.4 Nuclear-ensemble approximation. , 2.5 Emission spectrum -- 2.6 Comments on the line shapes -- 3 Spectrum decomposition -- 4 Computational details -- 5 Vertical spectra -- 5.1 Vertical excitation of furan -- 5.2 Vertical excitation of benzene -- 5.3 Vertical excitation and emission of 2-phenylfuran -- 6 Spectrum simulations -- 6.1 Absorption spectrum of furan -- 6.2 Absorption spectrum of benzene -- 6.3 Absorption spectrum of 2-phenylfuran -- 6.4 Emission spectrum of 2-phenylfuran -- 7 Conclusions -- Acknowledgments -- References -- Methods of continuous translation of the origin of the current density revisited -- Abstract -- Keywords -- 1 Introduction -- 2 The Rayleigh-Schro¨dinger approach to magnetic response properties -- 3 The electronic current density induced by a static magnetic field -- 3.1 Magnetizability and nuclear magnetic shielding tensors from electronic current density -- 3.2 Invariance of magnetizability, nuclear magnetic shielding and electronic current density in a gauge translation -- 4 Methods of continuous translation of the origin of the current density -- 5 Concluding remarks and outlook -- References -- Erratum to: Methods of continuous translation of the origin of the current density revisited -- A simple analysis of the influence of the solvent-induced electronic polarization on the 15N magnetic shielding of pyridine in water -- Abstract -- Keywords -- 1 Introduction -- 2 Methodology -- 3 Results -- 3.1 Solute polarization -- 3.2 Hydrogen bonds -- 3.3 Chemical shielding -- 4 Conclusions -- Acknowledgments -- References -- Theoretical simulations of the vibrational predissociation spectra of H5+ and D5+ clusters -- Abstract -- Keywords -- 1 Introduction -- 2 Coordinate system, model Hamiltonian operator, and computational details -- 3 Results and discussion -- 4 Summary and conclusions -- Acknowledgments -- References.