bluuebunny/crossref_metadata_2025_split huggingface dataset:
Time-accurate calculations with an implicit Euler /N avier-Stokes solver
Authors: Hoffren Jaakko , Siikonen Timo 
Published: November 2023

Abstract
Euler and Navier-Stokes solvers for steady flows have reached a stage of development where they can be applied to practical problems with a reasonable degree of effort. The required grid resolution and spatial discretization to obtain accurate results in certain types of applications are well known. Among the standard features of the modern codes are the use of a finite-volume formulation and second- or third-order accurate upwind differencing facilitated by the works of Roe and Van Leer. These concepts are also utilized in the thin-layer Navier-Stokes solver developed in the Laboratory of Aerodynamics of the Helsinki University of Technology (Siikonen et al. 1990).
Towards a cell-vertex multi-grid Navier-Stokes algorithm for three-dimensional structured/ unstructured meshes
Authors: Peace A J 
Published: November 2023

Abstract
The problem of predicting the flowfield around complex aircraft configurations continues to receive much interest within the aeronautical research community. To a great extent, the ability of a flow analysis method to examine increasingly complex geometries is paced by the mesh generation capability inherent to the method. In this respect, a number of different strategies have materialised over the past few years for discretising domains around complex configurations. One such strategy, and the one addressed here, is the structured/unstructured approach, whereby the flow-field is composed of regions of structured mesh (hexahedra) and regions of unstructured mesh (tetrahedra). As this approach has its origins in a much used block-structured (multi-block) method, Shaw et al. (1988), the hexahedral cells are contained within structured blocks. The background philosophy behind this approach to mesh generation is given in Shaw et al. (1990).
Handbook of Logic in Computer Science
Authors: Gabbay Dov M 
Published: November 2023

Abstract
The Handbook of Logic in Computer Science is a multi-volume work covering all major areas of application of logic to theoretical computer science. The Handbook comprises six volumes. Each volume contains five or six chapters, giving an in-depth overview of one of the major topics in the field. It is the result of many years of co-operative effort by some of the most eminent frontline researchers in the area. It will no doubt be the standard reference work in logic and theoretical computer science for years to come - essential reading for all those interested in theoretical computer science and logic. volumes cover the background to the subject in terms of mathematical and computational structures. The authors are chosen on an international basis and are leaders in the fields covered. The Handbook is a closely coordinated work which has been under development for the past five years.
Methods and Calculi for Deduction
Authors: Bibel W , Eder E 
Published: November 2023

Abstract
Logic has been presented in David Israel’s Chapter as a language to formalize problems arising in subareas of intellectics (and of other fields, for that matter). In Davis’ Chapter, it is shown that logic also supplies a relationship (denoted by |=) among different statements (orformulas) in that language. Note that there are actually many logics in the literature. As a default, we meanfirst-order logic unless explicitly specified otherwise. The formulas related this way to the empty set of formulas (i.e.ϕ |= F) play a particularly important role. They are calledvalid formulas. It turns out that in many cases a problem can be reformulated as a logical formula to be proved valid. For this reason one often speaks of ‘theorem proving’ where in effect solving problems, as those just referred to, is the issue.
Classical vs Non-classical Logics (The Universality of Classical Logic)
Authors: Gabbay D M 
Published: November 2023

Abstract
This chapter addresses the problem of whether classical logic can be used as a universal system of logic and whether it can be applied, profitably and sensibly, in all areas where logic needs to be applied. More specifically, we focus on modal and temporal logics and ask whether the use of such special logics, as compared with the use of classical logic, is advantageous. We examine what we lose and what we gain if we use classical logic instead of specialized logics to describe and reason about the same (e.g. temporal) phenomena.
Introduction And Overview
Authors: Gabbay Dov M , Reynolds Mark A , Finger Marcelo 
Published: November 2023

Abstract
The sections below give an overview of the contents of this book. This volume, Volume 2 in the series, deals with the more applicable aspects of temporal logics. Volume 1 gave the basic concepts and methods and concentrated more on the expressive power of temporal languages, their axiomatization, their dimension and their decidability. Now we are ready to deal with some aspects of their applications. The first four chapters of the present volume continue with the more theoretical presentation, covering automata, branching time and labelled deduction. The rest of the book progresses in the direction of temporal databases, temporal execution and programming, actions and planning. For details, see the following sections of this chapter.
The Metatem Programming Language
Authors: Gabbay Dov M , Reynolds Mark A , Finger Marcelo 
Published: November 2023

Abstract
METATEM is really a paradigm for programming languages rather than one particular language. There are three basic principles:
The versions of METATEM described in [Barringer et al., 1989], [Finger et al., 1993], [Fisher and Barringer, 1991], [Fisher, 1993], [Reynolds, 1995], [Barringer et al., 1996) and [Reynolds, 1997) use the temporal languages PML and FMO with Until and Since.
Propositional quantifiers and fixed point operators
Authors: Gabbay Dov M , Hodkinson Ian , Reynolds Mark 
Published: November 2023

Abstract
In this chapter we investigate the two related topics of propositional quantifiers and fixed point operators. In sections 8.1-8.3 we look at languages in which there are formulae ∀xA and ∃xA where x behaves in A as a proposition. There are different semantics depending on what we mean by a ‘proposition’, i.e. what we let q range over. In any case we obtain such expressive languages that they are not directly useful for computation. In the rest of the chapter we look at some very useful sublanguages in which quantifiers of the form LFPqA are used to build formulae and in which their semantics are defined as the least fixed point of certain operators. As we will see, these fixed point languages allow a sort of inductive definition of new propositions.
Further expressive completeness results
Authors: Gabbay Dov M , Hodkinson Ian , Reynolds Mark 
Published: November 2023

Abstract
In this chapter we prove the same result as we did in the last. First we will examine the idea of gaps in the flow of time in some detail. Then we will introduce some new connectives to talk about such gaps and use the expressive completeness of the Stavi connectives to deduce expressive completeness results for these new connectives. We also present some axiomatizations of these connectives. Finally, we prove the expressive completeness of the Stavi connectives again but this time we do not use separation. Instead we present a more direct proof using games. Generalizations of such a proof may be useful in cases where separation is difficult to show.
Modal Logics
Authors: Chagrov Alexander , Zakharyaschev Michael 
Published: November 2023

Abstract
When discussing in Section 2.1 the meaning of intuitionistic connectives, we used in our language-a metalanguage with respect to ℒ-the undefined notion “proof’. Making the proof interpretation somewhat rougher, we can treat, for example, the intuitionistic formulap--→qVras the proposition
Canonical Formulas
Authors: Chagrov Alexander , Zakharyaschev Michael 
Published: November 2023

Abstract
In Sections 2.5 and 3.5 we characterized the geometry of Kripke frames validating some intuitionistic and modal formulas by imposing first order conditions on their accessibility relations. However, as was shown in Section 6.2, there exist formulas which have no first order equivalents. In this chapter we try another, purely frame-theoretic approach to the characterization problem which uses such notions as subframe, reduction, etc. Unfortunately, this approach is not universal either. But its limitation is of a different kind: it characterizes onlytransitivegeneral frames, but for every modal and intuitionistic formula. So all frames in this chapter are assumed to betransitive.
The Disjunction Property and Halldén Completeness
Authors: Chagrov Alexander , Zakharyaschev Michael 
Published: November 2023

Abstract
Recall that a modal logicLhas the (modal disjunction propertyif, for everyn ≥ 1 and all formulas φ1, … ,φn, And a (modal or superintuitionistic) logicLis said to beHalldén completeif (15.1) holds for all φand ψcontaining no common variables
Correspondence between operational and denotational semantics: the full abstraction problem for PCF*
Authors: Ong C -H L 
Published: November 2023

Abstract
This chapter addresses a number of computationally relevant mathematical problems arising from the relationship between operational and denotational semantics of higher-type (or higher-order) sequential functional programming languages. We choose Scott’s language PCF (which stands for Programs for Computable Functions) as the vehicle for developing the leading ideas.
Cardinal Arithmetic
Authors: Shelah Saharon 
Published: November 2023

Abstract
I am always very enthusiastic about my last work, but since Dec 87 I am enthusiastic mainly about the work presented here. Let me try to share this with you, the reader. If we interpret “true” by “is provable in ZFC” (the usual axioms of set theory), as I do, then a large part of set theory which is done today does not deal directly with true theorems-it deals, rather, with a huge machinery for building counterexamples (forcing possible universes) or with “thin” universes (inner models). Very often the answer to “can this happen?” is “it depends”. Now, I believe that this phenomenon is inevitable, and expresses a deep phase of the development of set theory, which resulted in many fascinating theorems (and also in quite a few proofs of mine). However, there is still some uneasiness about it. A way to express it is to say that if Cantor would have risen from his grave today, he would not just have problems understanding the proofs of modern theorems-he would not understand what the theorems actually say. We do not try to fight this prejudice here, as it works in our favour.
Nw+l Has A Jonsson Algebra [Sh 355]
Authors: Shelah Saharon 
Published: November 2023

Abstract
We advance our knowledge on the cofinality of products of regular cardinals and give several applications; for example there is a Jonsson algebra on Nw+l and Nw+l -c.c. is not productive. This chapter introduces pp (using pcf’s) as our substitute to exponentiation and advances our understanding of pcf to have a considerable number of applications.
There Are Jonsson Algebras In Many Inaccessible Cardinals [Sh 365]
Authors: Shelah Saharon 
Published: November 2023

Abstract
Here we prove (in ZFC) that there is a Jonsson algebra on , λ if: , λ is an inaccessible not w-Mahlo or just, λ is an inaccessible (not necessarily strong limit) cardinal which has a stationary subset not reflecting in any inaccessible cardinals. We also prove this for many successor of singulars.
Random Walks In The Continuum Limit
Authors: Hughes Barry d. 
Published: November 2023

Abstract
A key issue in the theories of random processes and random systems, and perhaps the key issue so far as their relevance to physics and technology is concerned, is the resolution of the following question. What does randomness in the small conspire to produce in the large? We address this question for random walk processes, for which the answers are well understood, in the present chapter. The canonical application of random walk models is to the theory of Brownian movement.KKKKKKKKKKK M Y BI
Introduction To Volume 2
Authors: Hughes Barry D 
Published: November 2023

Abstract
In Volume 1 of this work, we gave a self-contained introduction to random walks and related processes. In these processes, ‘disorder’ is temporal in nature. Typically, a moving particle (the random walker) takes steps at fixed time intervals, and at each step a random direction is chosen, resulting in a chaotic trajectory. The present volume, in contrast, addresses models in which disorder is frozen in space. We describe such models as random environments.
An Introduction To Percolation Theory
Authors: Hughes Barry D 
Published: November 2023

Abstract
The basic ideas of percolation theory were anticipated in the early 1940s in the theory of polymer gelation (Flory 1941, Stockmayer 1944) and in the theory of branching processes (Good 1949). However, the genesis of percolation theory may be attributed justly to Broadbent (1954) in the published discussion of a paper by Hammersley and Morton (1954) on Monte Carlo methods. The early history of the subject is discussed by Hammersley (1983): Broadbent was at that time working at the British Coal Utilization Research Association on the design of gas masks for use in coal mines.
Algebraic Riccati Equations
Authors: Lancaster Peter , Rodman Leiba 
Published: November 2023

Abstract
This book provides a careful treatment of the theory of algebraic Riccati equations. It consists of four parts: the first part is a comprehensive account of necessary background material in matrix theory including careful accounts of recent developments involving indefinite scalar products and rational matrix functions. The second and third parts form the core of the book and concern the solutions of algebraic Riccati equations arising from continuous and discrete systems. The geometric theory and iterative analysis are both developed in detail. The last part of the book is an exciting collection of eight problem areas in which algebraic Riccati equations play a crucial role. These applications range from introductions to the classical linear quadratic regulator problems and the discrete Kalman filter to modern developments in HD*W*w control and total least squares methods.
Gemetric Theory the Real Case
Authors: Lancaster Peter , Rodman Leiba 
Published: November 2023

Abstract
Using the geometric methods developed in Chapter 7 we now study symmetric Riccati equations of the form (7.2.1) for which the coefficient matrices A, C, D are assumed to be real and, accordingly, only real solutions X are sought. The theory will parallel that of Chapter 7 and so, when the real case does not differ significantly from the complex case already investigated, proofs may be omitted or merely outlined. However, for some purposes it will be necessary to call on the analysis of real matrix pairs carried out in Section 2.7 and Chapter 3.
Perturbation Theory for Discrete Algebraic Riccati Equations
Authors: Lancaster Peter , Rodman Leiba 
Published: November 2023

Abstract
Taking advantage of the geometric theory for the discrete algebraic Riccati equation developed in Chapter 12, as well as the comparison theorems of Chapter 13, we can now study the behaviour of hermitian solutions of discrete algebraic Riccati equations under small perturbations of the coefficients of these equations. The emphasis is on the behaviour of extremal (minimal and maximal) solutions. Their behaviour as functions of the coefficients is studied here as well. The material of this chapter is, of course, the analogue of that in Chapter 11 and is developed here for the DARE of equation (12.2.1) rather than the CARE of equation (7.2.1).
Discrete Algebraic Riccati Equations and Matrix Pencils
Authors: Lancaster Peter , Rodman Leiba 
Published: November 2023

Abstract
The use of the matrix T makes it necessary, of course, to assume that A is invertible. This assumption can be avoided by relating the DARE to a J-unitary pencil (see Section 2.9) of the form rather than the pencil λI −T. When A is not invertible this pencil has an eigenvalue at infinity, a phenomenon which cannot arise in a classical eigenvalue problem. There are other advantages in the matrix pencil technique which will be mentioned in the sequel. Some of the basic ideas and results are described in this chapter but, in the authors’ view, the theory cannot be described as complete, and is still a developing area of research.
Parameter Optimization Algorithms
Authors: Bishop Christopher M 
Published: November 2023

Abstract
In previous chapters, the problem of learning in neural networks has been formulated in terms of the minimization of an error function E. This error is a function of the adaptive parameters (weights and biases) in the network, which we can conveniently group together into a single W-dimensional weight vector w with components. In Chapter 4 it was shown that, for a multi-layer perceptron, the derivatives of an error function with respect to the network parameters can be obtained in a computationally efficient way using back-propagation. We shall see that the use of such gradient information is of central importance in finding algorithms for network training which are sufficiently fast to be of practical use for large-scale applications.
Pre-Processing And Feature Extraction
Authors: Bishop Christopher M 
Published: November 2023

Abstract
Since neural networks can perform essentially arbitrary non-linear functional mappings between sets of variables, a single neural network could, in principle, be used to map the raw input data directly onto the required final output values. In practice, for all but the simplest problems, such an approach will generally give poor results for a number of reasons which we shall discuss below. For most applications it is necessary first to transform the data into some new representation before training a neural network. To some extent, the general-purpose nature of a neural network mapping means that less emphasis has to be placed on careful optimization of this pre-processing than would be the case with simple linear techniques, for instance. Nevertheless, in many practical applications the choice of pre-processing will be one of the most significant factors in determining the performance of the final system.
Formal Bases for Dataflow Analysis of Logic Programs
Authors: Debray Saumya K 
Published: November 2023

Abstract
Compile-time dataflow analysis finds a variety of applications, such as compile-time optimization, program parallelization, testing, program transformation and specialization, and program verification. This chapter gives a broad overview of the field of dataflow analysis of logic programs. Starting with a general discussion of abstract interpretation, a formal framework that underlies much of the work on static program analysis, it discusses some of the wide variety of frameworks that have been proposed for the analysis of logic programs, considers the relationship between complexity and precision of analysis, and examines some specific analyses that have been proposed in the literature.
Modular Termination Proofs for Logic and Pure PROLOG Programs
Authors: Apt Krzysztof R , Pedreschi Dino 
Published: November 2023

Abstract
We provide a uniform and simplified presentation of the methods of Bezem (1993) (first published as (Bezem 1989)) and of Apt and Pedreschi (1993) (first published as (Apt and Pedreschi 1990)) for proving termination of logic and PROLOG programs. Then we show how these methods can be refined so that they can be used in a modular way.
Interior point methods
Authors: Roos Cornelis , Vial Jean-Philippe 
Published: November 2023

Abstract
The interest in interior point methods for linear programming emerged from Karmarkar’s contribution in 1984. This field has soon become one of the most active in the area of mathematical programming. It introduced new ideas and techniques that now have received their own place among the basic tools in optimization. In this chapter we intend to provide an introduction to the theory of interior point methods.
Diagrams and the Concept of Logical System
Authors: Barwise Jon , Hammer* Eric 
Published: November 2023

Abstract
This volume is devoted to an interesting and important question: what is a logical system? The question is interesting because a good answer could do much to systematize and unify a bewildering logical landscape; it is important because if an answer were widely accepted, it could help guide research in logic in the years to come. In attempting to answer this question, there are various approaches that could be taken. One would be to look at the things people have called logical systems and try to develop a natural framework which would encompass most or many of these, and then explore the consequences of the framework, seeing what else falls under the framework and what the consequences of the general notion happen to be. This was basically the approach taken, for example, in Barwise [1], one of the early attempts to develop such a framework.
General Logics and Logical Frameworks
Authors: Martí-Oliet Narciso , Meseguer José 
Published: November 2023

Abstract
This chapter summarizes a theory of general logics first introduced in [39], in which different aspects, or components, of a logic such as its entailment relation, its proof theory, and its model theory are axiomatized. For the model-theoretic component, the theory of institutions of Goguen and Burstall [24] is adopted. Combinations of several such aspects of a logic are also supported by the theory. Special importance is given to the notion of mapping between logics that preserves the logical structure of some aspect, such as the entailment relation, or the satisfaction relation for the models. Such maps play for logics a role analogous to that played by group homomorphisms for groups. The notion of a logical framework, understood as a logic : ℱ in which many other logics can be represented, is then expressed in terms of appropriate representation maps ℒ → ℱ. The particular logical framework provided by rewriting logic [40] is introduced and discussed, and some of its good properties for representing logics and for reflecting aspects of its own metatheory are explained.
The Emperor’s New Clothes: Some Recurring Problems in the Formal Analysis of Counterfactuals
Authors: Hansson Sven Ove 
Published: November 2023

Abstract
Three major formal approaches to counterfactual conditionals are analysed: the derivability approach (Chisholm, Goodman, Mackie), the worldselection approach (Stalnaker, Lewis), and the belief revision approach (Harper, Levi, Gardenfors). The three approaches are shown to be essentially interchangeable from the point of view of formal logic. Furthermore, they are shown to have three important limitations in common, namely non-deductiveness, circularity, and shift ability. It is argued that despite these limitations, logical analysis can contribute to philosophical understanding of counterfactual conditionals.
Early Analysis
Authors: Russ Steve 
Published: November 2023

Abstract
By the end of the eighteenth century the algebraic and infinitesimal methods that had been used to solve the geometry problems of the seventeenth century had proved so successful in a wide range of physical problems that, under the general heading ‘analysis’, they had become the dominant part of mathematics. The intuitive concepts of space, time, and motion, long associated with geometry and mechanics, were losing ground to the more formal manipulation of functions and equations by the methods of calculus. It was perhaps inevitable after the advent of analytic geometry that these developments should lead, during the eighteenth century, to analytical or ‘rational’ mechanics. In the Preface to his Méchanique analytique (1788) Lagrange wrote: