Search

We establish a list of characterizations of bounded twin-width for hereditary classes of totally ordered graphs: as classes of at most exponential growth studied in enumerative combinatorics, as monadically NIP classes studied in model theory, as classes that do not transduce the class of all graphs studied in finite model theory, and as classes for which model checking first-order logic is fixed-parameter tractable studied in algorithmic graph theory. This has several consequences. First, it allows us to show that every hereditary class of ordered graphs either has at most exponential growth, or has at least factorial growth. This settles a question first asked by Balogh et al. [5] on the growth of hereditary classes of ordered graphs, generalizing the Stanley-Wilf conjecture/Marcus-Tardos theorem. Second, it gives a fixed-parameter approximation algorithm for twin-width on ordered graphs. Third, it yields a full classification of fixed-parameter tractable first-order model checking on hereditary classes of ordered binary structures. Fourth, it provides a model-theoretic characterization of classes with bounded twin-width. Finally, it settles the small conjecture [8] in the case of ordered graphs. [ABSTRACT FROM AUTHOR]

We prove near-optimal tradeoffs for quantifier depth (also called quantifier rank) versus number of variables in first-order logic by exhibiting pairs of n-element structures that can be distinguished by a k-variable firstorder sentence but where every such sentence requires quantifier depth at least nΩ(k/logk). Our tradeoffs also apply to first-order counting logic and, by the known connection to the k-dimensional Weisfeiler--Leman algorithm, imply near-optimal lower bounds on the number of refinement iterations. A key component in our proof is the hardness condensation technique introduced by Razborov in the context of proof complexity. We apply this method to reduce the domain size of relational structures while maintaining the minimal quantifier depth needed to distinguish them in finite variable logics. [ABSTRACT FROM AUTHOR]

The article examines a misconception in recent publications regarding Russell's theory of descriptions. It clarifies that the translations of English sentences containing definite descriptions into quantificational forms are incorrect. The article provides examples to illustrate the correct understanding of Russell's theory and addresses criticisms raised by other scholars. It also discusses the use of imaginary names in Russell's theory and the potential confusion between restrictive and non-restrictive relative clauses. The author suggests a correction to the formalization of a logical statement involving uniqueness. [Extracted from the article]

In this essay, I critically analyze Wittgenstein's dispensation with " = " in a correct concept-script. I argue inter alia (a) that in the Tractatus the alleged pseudo-character of sentences containing " = " or = -sentences remains largely unexplained and propose how it could be explained; (b) that at least in some cases of replacing = -sentences with equivalent identity-sign free sentences the use of the notion of a translation seems inappropiate; (c) that in the Tractatus it remains unclear how identity of the object as that which is expressed by identity of the sign should be understood specifically; (d) that there are = -sentences which have no obvious equivalent in Wittgenstein's novel notation; (e) that Wittgenstein's adherence to (non-relational) identity, although he dispenses with " = ", is probably motivated by his desire to ensure that the expressive power of an identity-sign free concept-script of first-order is on a par with standard first-order logic containing " = ". In the concluding section, I critically discuss some claims in Lampert and Säbel (The Review of Symbolic Logic, 14, 1–21, 2021) and defend Wehmeier's account of pseudo-sentences in the Tractatus (2012) against the objections they raise. [ABSTRACT FROM AUTHOR]

The interpretability of AI is just as important as its performance. In the LegalAI field, there have been efforts to enhance the interpretability of models, but a trade-off between interpretability and prediction accuracy remains inevitable. In this paper, we introduce a novel framework called LK-IB for compulsory measure prediction (CMP), one of the critical tasks in LegalAI. LK-IB leverages Legal Knowledge and combines an Interpretable model and a Black-box model to balance interpretability and prediction performance. Specifically, LK-IB involves three steps: (1) inputting cases into the first module, where first-order logic (FOL) rules are used to make predictions and output them directly if possible; (2) sending cases to the second module if FOL rules are not applicable, where a case distributor categorizes them as either "simple" or "complex"; and (3) sending simple cases to an interpretable model with strong interpretability and complex cases to a black-box model with outstanding performance. Experimental results demonstrate that the LK-IB framework provides more interpretable and accurate predictions than other state-of-the-art models. Given that the majority of cases in LegalAI are simple, the idea of model combination has significant potential for practical applications. [ABSTRACT FROM AUTHOR]

We describe the design, implementation and verification of an automated theorem prover for first-order logic with functions. The proof search procedure is based on sequent calculus and we formally verify its soundness and completeness in Isabelle/HOL using an existing abstract framework for coinductive proof trees. Our analytic completeness proof covers both open and closed formulas. Since our deterministic prover considers only the subset of terms relevant to proving a given sequent, we do the same when building a countermodel from a failed proof. Finally, we formally connect our prover with the proof system and semantics of the existing SeCaV system. In particular, the prover can generate human-readable SeCaV proofs which are also machine-verifiable proof certificates. The abstract framework we rely on requires us to fix a stream of proof rules in advance, independently of the formula we are trying to prove. We discuss the efficiency implications of this and the difficulties in mitigating them. [ABSTRACT FROM AUTHOR]

(Goodsell, Journal of Philosophical Logic, 51(1), 127-150 2022) establishes the noncontingency of sentences of first-order arithmetic, in a plausible higher-order modal logic. Here, the same result is derived using significantly weaker assumptions. Most notably, the assumption of rigid comprehension—that every property is coextensive with a modally rigid one—is weakened to the assumption that the Boolean algebra of properties under necessitation is countably complete. The results are generalized to extensions of the language of arithmetic, and are applied to answer a question posed by Bacon and Dorr (2024). [ABSTRACT FROM AUTHOR]

Despite their controversial ontological status, the discussion on arbitrary objects has been reignited in recent years. According to the supporting views, they present interesting and unique qualities. Among those, two define their nature: their assuming of values, and the way in which they present properties. Leon Horsten has advanced a particular view on arbitrary objects which thoroughly describes the earlier, arguing they assume values according to a sui generis modality, which he calls afthairetic. In this paper, we offer a general method for defining the minimal system of this modality for any given first-order theory, and possible extensions of it that incorporate further aspects of Horsten's account. The minimal system presents an unconventional inference rule, which deals with two different notions of derivability. For this reason and the failure of the Necessitation rule, in its full generality, the resulting system is non-normal. Then, we provide conditional soundness and completeness results for the minimal system and its extensions. [ABSTRACT FROM AUTHOR]

We present a general approach to quantified modal logics that can simulate most other approaches. The language is based on operators indexed by terms which allow to express de re modalities and to control the interaction of modalities with the first-order machinery and with non-rigid designators. The semantics is based on a primitive counterpart relation holding between n-tuples of objects inhabiting possible worlds. This allows an object to be represented by one, many, or no object in an accessible world. Moreover by taking as primitive a relation between n-tuples we avoid some shortcoming of standard individual counterparts. Finally, we use cut-free labelled sequent calculi to give a proof-theoretic characterisation of the quantified extensions of each first-order definable propositional modal logic. In this way we show how to complete many axiomatically incomplete quantified modal logics. [ABSTRACT FROM AUTHOR]

Here I show that the one-variable fragment of several first-order relevant logics corresponds to certain S5ish extensions of the underlying propositional relevant logic. In particular, given a fairly standard translation between modal and one-variable languages and a permuting propositional relevant logic L, a formula A of the one-variable fragment is a theorem of LQ (QL) iff its translation is a theorem of L5 (L.5). The proof is model-theoretic. In one direction, semantics based on the Mares-Goldblatt [15] semantics for quantified L are transformed into ternary (plus two binary) relational semantics for S5-like extensions of L (for a general presentation, see Seki [26-27]). In the other direction, a valuation is given for the full first-order relevant logic based on L into a model for a suitable S5 extension of L. I also discuss this work's relation to finding a complete axiomatization of the constant domain, non-general frame ternary relational semantics for which RQ is incomplete [11]. [ABSTRACT FROM AUTHOR]

We study property testing of properties that are definable in first-order logic (FO) in the bounded-degree graph and relational structure models. We show that any FO property that is defined by a formula with quantifier prefix ∃∗∀∗ is testable (i.e., testable with constant query complexity), while there exists an FO property that is expressible by a formula with quantifier prefix ∀∗∃∗ that is not testable. In the dense graph model, a similar picture is long known (Alon, Fischer, Krivelevich, Szegedy, Combinatorica 2000), despite the very different nature of the two models. In particular, we obtain our lower bound by an FO formula that defines a class of bounded-degree expanders, based on zig-zag products of graphs. We expect this to be of independent interest. We then use our class of FO definable bounded-degree expanders to answer a long-standing open problem for proximity-oblivious testers (POTs). POTs are a class of particularly simple testing algorithms, where a basic test is performed a number of times that may depend on the proximity parameter, but the basic test itself is independent of the proximity parameter. In their seminal work, Goldreich and Ron [STOC 2009; SICOMP 2011] show that the graph properties that are constant-query proximity-oblivious testable in the bounded-degree model are precisely the properties that can be expressed as a generalised subgraph freeness (GSF) property that satisfies the non-propagation condition. It is left open whether the non-propagation condition is necessary. We give a negative answer by showing that our property is a GSF property which is propagating. Hence in particular, our property does not admit a POT. For this result we establish a new connection between FO properties and GSF-local properties via neighbourhood profiles. [ABSTRACT FROM AUTHOR]

Deep neural networks, despite their capabilities, are constrained by the need for large-scale training data, and often fall short in generalisation and interpretability. Inductive logic programming (ILP) presents an intriguing solution with its data-efficient learning of first-order logic rules. However, ILP grapples with challenges, notably the handling of non-linearity in continuous domains. With the ascent of neuro-symbolic ILP, there's a drive to mitigate these challenges, synergising deep learning with relational ILP models to enhance interpretability and create logical decision boundaries. In this research, we introduce a neuro-symbolic ILP framework, grounded on differentiable Neural Logic networks, tailored for non-linear rule extraction in mixed discrete-continuous spaces. Our methodology consists of a neuro-symbolic approach, emphasising the extraction of non-linear functions from mixed domain data. Our preliminary findings showcase our architecture's capability to identify non-linear functions from continuous data, offering a new perspective in neural-symbolic research and underlining the adaptability of ILP-based frameworks for regression challenges in continuous scenarios. [ABSTRACT FROM AUTHOR]

It is shown that Holliday's propositional Fundamental Logic is decidable in polynomial time and that first-order Fundamental Logic is decidable in double-exponential time. The proof also yields a double-exponential–time decision procedure for first-order orthologic. [ABSTRACT FROM AUTHOR]

We study the connections between the notions of combinatorial discrepancy and graph degeneracy. In particular, we prove that the maximum discrepancy over all subgraphs H of a graph G of the neighborhood set system of H is sandwiched between Ω (log ⁡ deg (G)) and O (deg (G)) , where deg (G) denotes the degeneracy of G. We extend this result to inequalities relating weak coloring numbers and discrepancy of graph powers and deduce a new characterization of bounded expansion classes. Then we switch to a model theoretical point of view, introduce pointer structures, and study their relations to graph classes with bounded expansion. We deduce that a monotone class of graphs has bounded expansion if and only if all the set systems definable in this class have bounded hereditary discrepancy. Using known bounds on the VC-density of set systems definable in nowhere dense classes we also give a characterization of nowhere dense classes in terms of discrepancy. As consequences of our results, we obtain a corollary on the discrepancy of neighborhood set systems of edge colored graphs, a polynomial-time algorithm to compute ε -approximations of size O (1 / ε) for set systems definable in bounded expansion classes, an application to clique coloring, and even the non-existence of a quantifier elimination scheme for nowhere dense classes. [ABSTRACT FROM AUTHOR]

Decidability of monadic first-order classical logic was established by L¨owenheim in 1915. The proof made use of a semantic argument and a purely syntactic proof has never been provided. In the present paper we introduce a syntactic proof of decidability of monadic first-order logic in innex normal form which exploits G3- style sequent calculi. In particular, we introduce a cut- and contraction-free calculus having a (complexity-optimal) terminating proof-search procedure. We also show that this logic can be faithfully embedded in the modal logic T. [ABSTRACT FROM AUTHOR]

Lewis (The Journal of Philosophy, 65(5), 113–126, 1968) attempts to provide an account of modal talk in terms of the resources of counterpart theory, a first-order theory that eschews transworld identity. First, a regimentation of natural language modal claims into sentences of a formal first-order modal language L is assumed. Second, a translation scheme from L-sentences to sentences of the language of the theory is provided. According to Hazen (The Journal of Philosophy, 76(6), 319–338, 1979) and Fara & Williamson (Mind, 114(453), 1–30, 2005), the account cannot handle certain natural language modal claims involving a notion of actuality. The challenge has two parts. First, in order to handle such claims, the initial formal modal language that natural language modal claims are regimented into must extend L with something like an actuality operator. Second, certain ways that Lewis' translation scheme for L might be extended to accommodate an actuality operator are unacceptable. Meyer (Mind, 122(485), 27–42, 2013) attempts to defend Lewis' approach. First, Meyer holds that in order to handle such claims, the formal modal language L ∗ that we initially regiment our natural language claims into need not contain an actuality operator. Instead, we can make do with other resources. Next, Meyer provides an alternative translation scheme from L ∗ -sentences to sentences of an enriched language of counterpart theory. Unfortunately, Meyer's approach fails to provide an appropriate counterpart theoretic account of natural language modal claims. In this paper, I demonstrate that failure. [ABSTRACT FROM AUTHOR]

Let $\mathscr {C}$ be a class of finite and infinite graphs that is closed under induced subgraphs. The well-known Łoś–Tarski Theorem from classical model theory implies that $\mathscr {C}$ is definable in first-order logic by a sentence $\varphi $ if and only if $\mathscr {C}$ has a finite set of forbidden induced finite subgraphs. This result provides a powerful tool to show nontrivial characterizations of graphs of small vertex cover, of bounded tree-depth, of bounded shrub-depth, etc. in terms of forbidden induced finite subgraphs. Furthermore, by the Completeness Theorem, we can compute from $\varphi $ the corresponding forbidden induced subgraphs. This machinery fails on finite graphs as shown by our results: – There is a class $\mathscr {C}$ of finite graphs that is definable in first-order logic and closed under induced subgraphs but has no finite set of forbidden induced subgraphs. – Even if we only consider classes $\mathscr {C}$ of finite graphs that can be characterized by a finite set of forbidden induced subgraphs, such a characterization cannot be computed from a first-order sentence $\varphi $ that defines $\mathscr {C}$ and the size of the characterization cannot be bounded by $f(|\varphi |)$ for any computable function f. Besides their importance in graph theory, the above results also significantly strengthen similar known theorems for arbitrary structures. [ABSTRACT FROM AUTHOR]

This paper analyses and compares some of the automated reasoners that have been used in recent research for compliance checking. Although the list of the considered reasoners is not exhaustive, we believe that our analysis is representative enough to take stock of the current state of the art in the topic. We are interested here in formalizations at the first-order level. Past literature on normative reasoning mostly focuses on the propositional level. However, the propositional level is of little usefulness for concrete LegalTech applications, in which compliance checking must be enforced on (large) sets of individuals. Furthermore, we are interested in technologies that are freely available and that can be further investigated and compared by the scientific community. In other words, this paper does not consider technologies only employed in industry and/or whose source code is non-accessible. This paper formalizes a selected use case in the considered reasoners and compares the implementations, also in terms of simulations with respect to shared synthetic datasets. The comparison will highlight that lot of further research still needs to be done to integrate the benefits featured by the different reasoners into a single standardized first-order framework, suitable for LegalTech applications. All source codes are freely available at https://github.com/liviorobaldo/compliancecheckers, together with instructions to locally reproduce the simulations. [ABSTRACT FROM AUTHOR]

In this paper, the predicate counterparts, defined both axiomatically and semantically by means of Kripke frames, of the modal propositional logics |$\textbf {GL}$|⁠ , |$\textbf {Grz}$|⁠ , |$\textbf {wGrz}$| and their extensions are considered. It is proved that the set of semantical consequences on Kripke frames of every logic between |$\textbf {QwGrz}$| and |$\textbf {QGL.3}$| or between |$\textbf {QwGrz}$| and |$\textbf {QGrz.3}$| is |$\Pi ^1_1$| -hard even in languages with three (sometimes, two) individual variables, two (sometimes, one) unary predicate letters, and a single proposition letter. As a corollary, it is proved that infinite families of modal predicate axiomatic systems, based on the classical first-order logic and the modal propositional logics |$\textbf {GL}$|⁠ , |$\textbf {Grz}$|⁠ , |$\textbf {wGrz}$| are not Kripke complete. Both |$\Pi ^1_1$| -hardness and Kripke incompleteness results of the paper do not depend on whether the logics contain the Barcan formula. [ABSTRACT FROM AUTHOR]

Graph-based frames have been introduced as a logical framework which internalises an inherent boundary to knowability (referred to as 'informational entropy'), due, e.g. to perceptual, evidential or linguistic limits. They also support the interpretation of lattice-based (modal) logics as hyper-constructive logics of evidential reasoning. Conceptually, the present paper proposes graph-based frames as a formal framework suitable for generalising Pawlak's rough set theory to a setting in which inherent limits to knowability exist and need to be considered. Technically, the present paper establishes systematic connections between the first-order correspondents of Sahlqvist modal reduction principles on Kripke frames, and on the more general relational environments of graph-based and polarity-based frames. This work is part of a research line aiming at: (a) comparing and inter-relating the various (first-order) conditions corresponding to a given (modal) axiom in different relational semantics; (b) recognising when first-order sentences in the frame-correspondence languages of different relational structures encode the same 'modal content'; (c) meaningfully transferring relational properties across different semantic contexts. The present paper develops these results for the graph-based semantics, polarity-based semantics, and all Sahlqvist modal reduction principles. As an application, we study well known modal axioms in rough set theory (such as those corresponding to seriality, reflexivity, and transitivity) on graph-based frames and show that, although these axioms correspond to different first-order conditions on graph-based frames, their intuitive meaning is retained. This allows us to introduce the notion of hyperconstructivist approximation spaces as the subclass of graph-based frames defined by the first-order conditions corresponding to the same modal axioms defining classical generalised approximation spaces, and to transfer the properties and the intuitive understanding of different approximation spaces to the more general framework of graph-based frames. The approach presented in this paper provides a base for systematically comparing and connecting various formal frameworks in rough set theory, and for the transfer of insights across different frameworks. [ABSTRACT FROM AUTHOR]

In this paper, we introduce the notion of similarity monadic MTL-algebras and study some of their related basic algebraic properties. Then we introduce and investigate similarity monadic filters of similarity monadic MTL-algebras. In particular, by means of similarity monadic filters, we give some characterizations of representable similarity monadic MTL-algebras. Finally, we introduce the logic of similarity monadic MTL-algebras and prove the completeness of them. [ABSTRACT FROM AUTHOR]

Researchers and practitioners are increasingly embracing systems approaches to deal with the complexity of public service delivery and policy evaluation. However, there is little agreement on what exactly constitutes a systems approach, conceptually or methodologically. We review and critically synthesize systems literature from the fields of health, education, and infrastructure. We argue that the common theoretical core of systems approaches is the idea that multi-dimensional complementarities between a policy and other aspects of the policy context are the first-order problem of policy design and evaluation. We distinguish between macro-systems approaches, which focus on the collective coherence of a set of policies or institutions, and micro-systems approaches, which focus on how a single policy interacts with the context in which it operates. We develop a typology of micro-systems approaches and discuss their relationship to standard impact evaluation methods as well as to work in external validity, implementation science, and complexity theory. [ABSTRACT FROM AUTHOR]

The Language of Thought (LoT) hypothesis proposes that some collections of mental states and processes are symbol systems to explain language-like systematic properties of thought. Recent proponents of this hypothesis point to additional LoT-like properties in non-linguistic domains to claim that LoT remains the "best game in town" in terms of explanatory coverage. Nonetheless, LoT assumes but does not explain why/how symbolic representations connect to other (non-symbolic) formats. The perspective presented here is supposed to bridge this gap as a duality in a category theoretical sense: (perceptual) data are projected onto a base (conceptual) space in one direction, and in the opposite direction, these data are referenced by that space. Accordingly, perception is dual to conception. These constructions follow from a universal mapping principle affording an explanation for why/how symbolic and non-symbolic formats are connected: as the "best" possible transformation between the two forms-- so the slogan, LoT is universal. This view also sheds some light on the apparent pervasiveness of logic-like capacities across age-groups and species, and these constructions constitute special types of categories called toposes (topoi), and every topos has an interpretation in first-order logic. [ABSTRACT FROM AUTHOR]

In the present paper, we address the following general question in the framework of classical first-order logic. Assume that a certain mathematical principle can be formalized in a first-order language by a set E of conditional formulas of the form α (v) → β (v) . Given a base theory T, we can use the set of conditional formulas E to extend the base theory in two natural ways. Either we add to T each formula in E as a new axiom (thus obtaining a theory denoted by T + E ) or we extend T by using the formulas in E as instances of an inference rule (thus obtaining a theory denoted by T + E – Rule ). The theory T + E will be stronger than T + E – Rule , but how much stronger can T + E be? More specifically, is T + E conservative over T + E – Rule for theorems of some fixed syntactical complexity Γ ? Under very general assumptions on the set of conditional formulas E, we obtain two main conservation results in this regard. Firstly, if the formulas in E have low syntactical complexity with respect to some prescribed class of formulas Π and in the applications of E – Rule side formulas from the class Π and can be eliminated (in a certain precise sense), then T + E is ∀ B (Π) -conservative over T + E – Rule . Secondly, if, in addition, E is a finite set with m conditional sentences, then nested applications of E – Rule of a depth at most of m suffice to obtain ∀ B (Π) conservativity. These conservation results between axioms and inference rules extend well-known conservation theorems for fragments of first-order arithmetics to a general, purely logical framework. [ABSTRACT FROM AUTHOR]

We provide two proofs of the compactness theorem for extensions of first‐order logic based on team semantics. First, we build upon Lück's [16] ultraproduct construction for team semantics and prove a suitable version of Łoś' Theorem. Second, we show that by working with suitably saturated models, we can generalize the proof of Kontinen and Yang [13] to sets of formulas with arbitrarily many variables. [ABSTRACT FROM AUTHOR]

Recent advances in artificial intelligence (AI), combined with a proliferation in use, have led to a newfound emphasis on strengthening the global governance of AI. In this article, we assess the prospects for stronger global AI governance and consider potential pathways forward. We map the nascent landscape of international regimes focused on AI governance and conclude that a governance deficit remains due to the inadequacy of existing initiatives, gaps in the landscape and difficulties reaching agreement over more appropriate mechanisms. First-order cooperation problems stemming from interstate competition and second-order cooperation problems from dysfunctional international institutions problematize overcoming current deficiencies in global AI governance. In light of these cooperation problems, we evaluate two pathways for strengthening global AI governance: (a) developing new centralized international AI institution(s); and (b) strengthening coordination between, and capacities of, existing institutions. We argue that strengthening the existing weak 'regime complex' of international institutions is the more politically legitimate and viable path forward. Improving coordination between, and capacities of, existing international institutions governing AI would support inclusive and mutually reinforcing policy change that can mitigate a range of risks associated with these technologies. As first steps for strengthening the weak AI regime complex, we recommend that the OECD is foregrounded as a centre of expert AI knowledge so that it can facilitate peer pressure among states and harmonization of policies. We also encourage scrutiny of different nodes in the regime complex to ensure that they are fulfilling appropriate functions based on their democratic mandates. [ABSTRACT FROM AUTHOR]

We present a cut-free sequent calculus for a class of first-order theories in negation normal form which include coherent and co-coherent theories alike. All structural rules, including cut, are admissible. [ABSTRACT FROM AUTHOR]

We consider a model for the resilience analysis of interconnected critical infrastructures (ICIs) that describes the dependencies among the subsystems within the ICIs and their time-varying behavior. The model response is a function of uncertain inputs comprising ICIs design parameters and failure magnitudes of vulnerable elements in the system, etc. In this methodological paper, we present a systematic approach based on an innovative blend of methods to perform a sensitivity analysis for identifying the most relevant variables affecting the system resilience at different stages, during a disruptive event. The methods considered include the following: the use of the graphical representation of Cusunoro curves for a visualization of the impact of an input on the resilience metric and an understanding of whether the associated dependence is monotonic, increasing, or decreasing; the introduction of an ensemble of indicators related to different properties of the resilience metric to allow the prioritization of variable importance and avoid false negatives, meaning to regard a variable as non-influential when, instead, it plays a relevant role in the determination of the model response; the calculation of first-order variance-based sensitivity indices to have an appreciation on the relevance of interactions when inputs are independent; and a data approach to visually identify relevant second-order interactions. All the sensitivity methods considered are performed on a provided sample, and do not require additional model evaluations. They allow the analyst to post-process the data to extract, simultaneously, several desirable insights. The systematic approach proposed to apply these methods allows us to identify the model input variables and parameters that are not very relevant, while it enables the identification of the relevant ones which allows prioritizing interventions on the vulnerable elements of the system for its resilience at different stages during a disruptive event. Given the methodological nature of the work, a simplified infrastructure model describing an interconnected gas network and electric power grid is taken as case study: this allows us to show that the approach is straightforward to understand and implement, and the results obtained show the usefulness of the approach in providing meaningful insights that can be used by stakeholders and decision makers to inform strategies for the improvement of system resilience. By the application of the simplified ICIs model to the case study, it is shown that the approach can be straightforwardly implemented to identify the most relevant variables on system resilience and obtain the most important subsystems. The key factors which affect system resilience in multiple initial failures scenarios are found; this allows us to identify the key resilience improvement measurements, and their priorities. [ABSTRACT FROM AUTHOR]

Context is essential in virtually all human activities. Yet some logical notions seem to be context-free. For example, the nature of the universal quantifier, the very meaning of "all", seems to be independent of the context. At the same time, there are many quantifier expressions, and some are context-independent, while others are not. Similarly, purely logical consequence seems to be context-independent. Yet often we encounter strong inferences, good enough for practical purposes, but not valid. The two types of examples suggest a general problem: how to characterise the context-free logical concepts in their natural environment, that is, in the field of their context-dependent associates. A general Thesis on Quantifiers is formulated: among all quantifiers, the context-free ones are just those definable by the universal quantifier. The issue of inferences is treated following the approach introduced by Richard L. Epstein: valid ones are an extreme case, the result of the disappearance of context-dependence. This idea can be applied to an analysis of a form of abduction, called "reductive inference" in Polish literature on logic. A tentative Thesis on Inferences identifies the validity of a strong inference that is context-independent. [ABSTRACT FROM AUTHOR]

This work derives a theoretical value for the entropy of a Linear Additive Markov Process (LAMP), an expressive but simple model able to generate sequences with a given autocorrelation structure. Our research establishes that the theoretical entropy rate of a LAMP model is equivalent to the theoretical entropy rate of the underlying first-order Markov Chain. The LAMP model captures complex relationships and long-range dependencies in data with similar expressibility to a higher-order Markov process. While a higher-order Markov process has a polynomial parameter space, a LAMP model is characterised only by a probability distribution and the transition matrix of an underlying first-order Markov Chain. This surprising result can be explained by the information balance between the additional structure imposed by the next state distribution of the LAMP model, and the additional randomness of each new transition. Understanding the entropy of the LAMP model provides a tool to model complex dependencies in data while retaining useful theoretical results. To emphasise the practical applications, we use the LAMP model to estimate the entropy rate of the LastFM, BrightKite, Wikispeedia and Reuters-21578 datasets. We compare estimates calculated using frequency probability estimates, a first-order Markov model and the LAMP model, also considering two approaches to ensure the transition matrix is irreducible. In most cases the LAMP entropy rates are lower than those of the alternatives, suggesting that LAMP model is better at accommodating structural dependencies in the processes, achieving a more accurate estimate of the true entropy. [ABSTRACT FROM AUTHOR]

The automotive industry is increasingly dependent on computing systems with different critical requirements. The verification and validation methods for these systems are now leveraging complex AI methods, for which the decision algorithms introduce non-determinism, especially in autonomous driving. This paper presents a runtime verification technique agnostic to the target system, which focuses on monitoring spatio-temporal properties that abstract the evolution of objects' behavior in their spatial and temporal flow. First, a formalization of three known traffic rules (from the Vienna convention on road traffic) is presented, where a spatio-temporal logic fragment is used. Then, these logical expressions are translated to a monitoring model written in first-order logic, where they are processed by a non-linear satisfiability solver. Finally, the translation allows the solver to check the validity of the encoded properties according to an instance of a specific traffic scenario (a trace). The results obtained from our tool, which automatically generates a monitor from a formula, show that our approach is feasible for online monitoring in a real-world environment. [ABSTRACT FROM AUTHOR]

An algebraic characterisation is given of the Mares-Goldblatt semantics for quantified extensions of relevant and modal logics. Some features of this more general semantic framework are investigated, and the relations to some recent work in algebraic semantics for quantified extensions of non-classical logics are considered. [ABSTRACT FROM AUTHOR]

This paper develops the idea that valid arguments are equivalent to true conditionals by combining Kripke's theory of truth with the evidential account of conditionals offered by Crupi and Iacona. As will be shown, in a first-order language that contains a naïve truth predicate and a suitable conditional, one can define a validity predicate in accordance with the thesis that the inference from a conjunction of premises to a conclusion is valid when the corresponding conditional is true. The validity predicate so defined significantly increases our expressive resources and provides a coherent formal treatment of paradoxical arguments. [ABSTRACT FROM AUTHOR]

We investigate the decidability of first-order logic extensions. For example, it is established in Zolotov's works that a logic with a unary transitive closure operator for the one successor theory is decidable. We show that in a similar case, a logic with a unary partial fixed point operator is undecidable. For this purpose, we reduce the halting problem for the counter machine to the problem of truth of the underlying formula. This reduction uses only one unary nonnested partial fixed operator that is applied to a universal or existential formula. [ABSTRACT FROM AUTHOR]

The thesis that agents should calibrate their beliefs in the face of higher-order evidence—i.e., should adjust their first-order beliefs in response to evidence suggesting that the reasoning underlying those beliefs is faulty—is sometimes thought to be in tension with Bayesian approaches to belief update: in order to obey Bayesian norms, it's claimed, agents must remain steadfast in the face of higher-order evidence. But I argue that this claim is incorrect. In particular, I motivate a minimal constraint on a reasonable treatment of the evolution of self-locating beliefs over time and show that calibrationism is compatible with any generalized Bayesian approach that respects this constraint. I then use this result to argue that remaining steadfast isn't the response to higher-order evidence that maximizes expected accuracy. [ABSTRACT FROM AUTHOR]

Formalisms based on temporal logics interpreted over finite strict linear orders, known in the literature as finite traces, have been used for temporal specification in automated planning, process modelling, (runtime) verification and synthesis of programs, as well as in knowledge representation and reasoning. In this article, we focus on first-order temporal logic on finite traces. We first investigate preservation of equivalences and satisfiability of formulas between finite and infinite traces, by providing a set of semantic and syntactic conditions to guarantee when the distinction between reasoning in the two cases can be blurred. Moreover, we show that the satisfiability problem on finite traces for several decidable fragments of first-order temporal logic is ExpSpace-complete, as in the infinite trace case, while it decreases to NExpTime when finite traces bounded in the number of instants are considered. This leads also to new complexity results for temporal description logics over finite traces. Finally, we investigate applications to planning and verification, in particular by establishing connections with the notions of insensitivity to infiniteness and safety from the literature. [ABSTRACT FROM AUTHOR]

The k-spectrum is the set of all α > 0 such that G(n,n−α) does not obey the 0-1 law for FO sentences with quantifier depth at most k. In this article, we prove that the minimum k such that the k-spectrum is infinite equals 5. [ABSTRACT FROM AUTHOR]

The logic of information flows (LIF) has recently been proposed as a general framework in the field of knowledge representation. In this framework, tasks of procedural nature can still be modeled in a declarative, logic-based fashion. In this paper, we focus on the task of query processing under limited access patterns, a well-studied problem in the database literature. We show that LIF is well-suited for modeling this task. Toward this goal, we introduce a variant of LIF called “forward” LIF (FLIF), in a first-order setting. FLIF takes a novel graph-navigational approach; it is an XPath-like language that nevertheless turns out to be equivalent to the “executable” fragment of first-order logic defined by Nash and Lud¨ascher. One can also classify the variables in FLIF expressions as inputs and outputs. Expressions where inputs and outputs are disjoint, referred to as iodisjoint FLIF expressions, allow a particularly transparent translation into algebraic query plans that respect the access limitations. Finally, we show that general FLIF expressions can always be put into io-disjoint form. [ABSTRACT FROM AUTHOR]

We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides a formal programming language-theoretic foundation to the algorithmic processing of real numbers. In order to capture multi-valuedness, which is well-known to be essential to real number computation, we use a Plotkin powerdomain and make our programming language semantics computable and complete: all and only real functions computable in computable analysis can be realized in ERC. The base programming language supports real arithmetic as well as implicit limits; expansions support additional primitive operations (such as a user-defined exponential function). By restricting integers to Presburger arithmetic and real coercion to the ‘precision’ embedding Z ∋ p 7→ 2p ∈ R, we arrive at a first-order theory which we prove to be decidable and model-complete. Based on said logic as specification language for preconditions and postconditions, we extend Hoare logic to a sound (w.r.t. the denotational semantics) and expressive system for deriving correct total correctness specifications. Various examples demonstrate the practicality and convenience of our language and the extended Hoare logic. [ABSTRACT FROM AUTHOR]