SearcharxivSearch

arXiv subjects

Kees van Berkel

Publications and source records attributed to Kees van Berkel.

11 recordsLinked to original sources

The Cost and Network Limits of Space-Based AI Compute

This paper evaluates whether large-scale AI data centers deployed in low-Earth orbit (LEO) could become a cost-effective alternative to terrestrial facilities. The analysis compares orbital and ground-based systems across launch cost, power generation, cooling, radiation exposure, and atmospheric reentry, as well as compute-network performance. A key distinction is the shift from terrestrial Clos networks to space-based mesh networks using laser inter-satellite links. Using bisection bandwidth, bisection intensity, and roofline-style models, we show that while LEO-based inference may be feasible, training frontier-scale LLMs in orbit is unlikely to be competitive with terrestrial data centers.

cs.DC

The Varieties of Ought-Implies-Can and Deontic STIT Logic

STIT logic is a prominent framework for the analysis of multi-agent choice-making. In the available deontic extensions of STIT, the principle of Ought-implies-Can (OiC) fulfills a central role. However, in the philosophical literature a variety of alternative OiC interpretations have been proposed and discussed. This paper provides a modular framework for deontic STIT that accounts for a multitude of OiC readings. In particular, we discuss, compare, and formalize ten such readings. We provide sound and complete sequent-style calculi for all of the various STIT logics accommodating these OiC principles. We formally analyze the resulting logics and discuss how the different OiC principles are logically related. In particular, we propose an endorsement principle describing which OiC readings logically commit one to other OiC readings.

cs.LO

A Appropriate Probability Model for the Bell Experiment

The Bell inequality constrains the outcomes of measurements on pairs of distant entangled particles. The Bell contradiction states that the Bell inequality is inconsistent with the calculated outcomes of these quantum experiments. This contradiction led many to question the underlying assumptions, viz. so-called realism and locality. The probability model underlying the Bell inequality is generally left implicit. We propose an explicit probability model for the CHSH version of the Bell experiment. This model has only two simultaneously observable detector settings per measurement, and therefore does not assume realism. The quantum expectation now becomes a conditional expectation, given the two detector settings. This probability model is in full agreement with both quantum mechanics and experiments. As a result, the model satisfies the Bell inequality; there are no so-called violations. We extend this model to include a hidden variable. This extended model is not Bell-separable. This non-separability implies that the model is non-deterministic or non-local (or both).

quant-ph

Experiments with Schrödinger Cellular Automata

We derive a class of cellular automata for the Schrödinger Hamiltonian, including scalar and vector potentials. It is based on a multi-split of the Hamiltonian, resulting in a multi-step unitary evolution operator in discrete time and space. Experiments with one-dimensional automata offer quantitative insight in phase and group velocities, energy levels, related approximation errors, and the evolution of a time-dependent harmonic oscilator. The apparent effects of spatial waveform aliasing are intriguing. Interference experiments with two-dimensional automata include refraction, Davisson-Germer, Mach-Zehnder, single & double slit, and Aharonov-Bohm.

quant-ph

Proof Theory and Decision Procedures for Deontic STIT Logics

This paper provides a set of cut-free complete sequent-style calculi for deontic STIT ('See To It That') logics used to formally reason about choice-making, obligations, and norms in a multi-agent setting. We leverage these calculi to write a proof-search algorithm deciding deontic, multi-agent STIT logics with (un)limited choice and introduce a loop-checking mechanism to ensure the termination of the algorithm. Despite the acknowledged potential for deontic reasoning in the context of autonomous, multi-agent scenarios, this work is the first to provide a syntactic decision procedure for this class of logics. Our proof-search procedure is designed to provide verifiable witnesses/certificates of the (in)validity of formulae, which permits an analysis of the (non)theoremhood of formulae and act as explanations thereof. We show how the proof system and decision algorithm can be used to automate normative reasoning tasks such as duty checking (viz. determining an agent's obligations relative to a given knowledge base), compliance checking (viz. determining if a choice, considered by an agent as potential conduct, complies with the given knowledge base), and joint fulfillment checking (viz. determining whether under a specified factual context an agent can jointly fulfill all their duties).

cs.LO

A logical analysis of instrumentality judgments: means-end relations in the context of experience and expectations

This article proposes the use of temporal logic for an analysis of instrumentality inspired by the work of G.H. von Wright. The first part of the article contains the philosophical foundations. We discuss von Wright's general theory of agency and his account of instrumentality. Moreover, we propose several refinements to this framework via rigorous definitions of the core notions involved. In the second part, we develop a logical system called Temporal Logic of Action and Expectations (TLAE). The logic is inspired by a fragment of propositional dynamic logic based on indeterministic time. The system is proven to be weakly complete relative to its given semantics. We then employ TLAE to formalise and analyse the instrumentality relations defined in the first part of the paper. Last, we point out philosophical implications and possible extensions of our work.

math.LO

The Role of Time, Weather and Google Trends in Understanding and Predicting Web Survey Response

In the literature about web survey methodology, significant efforts have been made to understand the role of time-invariant factors (e.g. gender, education and marital status) in (non-)response mechanisms. Time-invariant factors alone, however, cannot account for most variations in (non-)responses, especially fluctuations of response rates over time. This observation inspires us to investigate the counterpart of time-invariant factors, namely time-varying factors and the potential role they play in web survey (non-)response. Specifically, we study the effects of time, weather and societal trends (derived from Google Trends data) on the daily (non-)response patterns of the 2016 and 2017 Dutch Health Surveys. Using discrete-time survival analysis, we find, among others, that weekends, holidays, pleasant weather, disease outbreaks and terrorism salience are associated with fewer responses. Furthermore, we show that using these variables alone achieves satisfactory prediction accuracy of both daily and cumulative response rates when the trained model is applied to future unseen data. This approach has the further benefit of requiring only non-personal contextual information and thus involving no privacy issues. We discuss the implications of the study for survey research and data collection.

cs.SI

Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics

This work provides proof-search algorithms and automated counter-model extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for STIT logics. A new class of cut-free complete labelled sequent calculi G3LdmL^m_n, for multi-agent STIT with at most n-many choices, is introduced. We refine the calculi G3LdmL^m_n through the use of propagation rules and demonstrate the admissibility of their structural rules, resulting in auxiliary calculi Ldm^m_nL. In the single-agent case, we show that the refined calculi Ldm^m_nL derive theorems within a restricted class of (forestlike) sequents, allowing us to provide proof-search algorithms that decide single-agent STIT logics. We prove that the proof-search algorithms are correct and terminate.

cs.LO

A Neutral Temporal Deontic STIT Logic

In this work we answer a long standing request for temporal embeddings of deontic STIT logics by introducing the multi-agent STIT logic TDS. The logic is based upon atemporal utilitarian STIT logic. Yet, the logic presented here will be neutral: instead of committing ourselves to utilitarian theories, we prove the logic TDS sound and complete with respect to relational frames not employing any utilitarian function. We demonstrate how these neutral frames can be transformed into utilitarian temporal frames, while preserving validity. Last, we discuss problems that arise from employing binary utility functions in a temporal setting.

cs.LO

Cut-free Calculi and Relational Semantics for Temporal STIT Logics

We present cut-free labelled sequent calculi for a central formalism in logics of agency: STIT logics with temporal operators. These include sequent systems for Ldm, Tstit and Xstit. All calculi presented possess essential structural properties such as contraction- and cut-admissibility. The labelled calculi G3Ldm and G3TSTIT are shown sound and complete relative to irreflexive temporal frames. Additionally, we extend current results by showing that also XSTIT can be characterized through relational frames, omitting the use of BT+AC frames.

cs.LO

Appendix for: Cut-free Calculi and Relational Semantics for Temporal STIT logics

This paper is an appendix to the paper "Cut-free Calculi and Relational Semantics for Temporal STIT logics" by Berkel and Lyon, 2019. It provides the completeness proof for the basic STIT logic Ldm (relative to irreflexive, temporal Kripke STIT frames) as well as gives the derivation of the independence of agents axiom for the logic Xstit.

cs.LO