The notion of program verification appears to trade upon an equivocation. Algorithms, as logical structures, are appropriate subjects for deductive verification. Programs, as causal models of those structures, are not. The success of program verification as a generally applicable and completely reliable method for guaranteeing program performance is not even a theoretical possibility.

In this paper I attempt to cast the current program verification debate within a more general perspective on the methodologies and goals of computer science. I show, first, how any method involved in demonstrating the correctness of a physically executing computer program, whether by testing or formal verification, involves reasoning that is defeasible in nature. Then, through a delineation of the senses in which programs can be run as tests, I show that the activities of testing (...) and formal verification do not necessarily share the same goals and thus do not always constitute alternatives. The testing of a program is not always intended to demonstrate a program's correctness. Testing may seek to accept or reject nonprograms including algorithms, specifications, and hypotheses regarding phenomena. The relationship between these kinds of testing and formal verification is couched in a more fundamental relationship between two views of computer science, one properly containing the other. (shrink)

A proof of ‘correctness’ for a mathematical algorithm cannot be relevant to executions of a program based on that algorithm because both the algorithm and the proof are based on assumptions that do not hold for computations carried out by real-world computers. Thus, proving the ‘correctness’ of an algorithm cannot establish the trustworthiness of programs based on that algorithm. Despite the (deceptive) sameness of the notations used to represent them, the transformation of an algorithm into an executable program (...) is a wrenching metamorphosis that changes a mathematical abstraction into a prescription for concrete actions to be taken by real computers. Therefore, it is verification of program executions (processes) that is needed, not of program texts that are merely the scripts for those processes. In this view, verification is the empirical investigation of: (a) the behavior that programs invoke in a computer system and (b) the larger context in which that behavior occurs. Here, deduction can play no more, and no less, a role than it does in the empirical sciences. (shrink)

How are the properties of computer programs proved? We discuss three approaches in this article: inductive invariants, functional semantics, and explicit semantics. Because the first approach has received by far the most attention, it has produced the most impressive results to date. However, the field is now moving away from the inductive invariant approach.

Fetzer famously claims that program verification is not even a theoretical possibility, and offers a certain argument for this far-reaching claim. Unfortunately for Fetzer, and like-minded thinkers, this position-argument pair, while based on a seminal insight that program verification, despite its Platonic proof-theoretic airs, is plagued by the inevitable unreliability of messy, real-world causation, is demonstrably self-refuting. As I soon show, Fetzer is like the person who claims: ‘My sole claim is that every claim expressed by (...) an English sentence and starting with the phrase “My sole claim” is false’. Or, more accurately, such thinkers are like the person who claims that modus tollens is invalid, and supports this claim by giving an argument that itself employs this rule of inference. (shrink)

The issue of proper functioning of operative computing and the utility of program verification, both in general and of specific methods, has been discussed a lot. In many of those discussions, attempts have been made to take mathematics as a model of knowledge and certitude achieving, and accordingly infer about the suitable ways to handle computing. I shortly review three approaches to the subject, and then take a stance by considering social factors which affect the epistemic status of (...) both mathematics and computing. I use the analogy between mathematics and computing in reverse—that is to say, I consider operative computing as a form of making mathematics, and so attempt to learn from computing to mathematics in general. I conclude that mathematics engineering is a field to be both developed for practical improvement of doing mathematics and taken into consideration while philosophizing about mathematics as well. (shrink)

Theorem 1 states a negative result about the classical semantics j=! of program schemes. Theorem 2 investigates the reason for this. We conclude that Theorem 2 justies the Henkin-type semantics j= for which the opposite of the present Theorem 1 was proved in [1]{[3] and also in a dierent form in part III of [5]. The strongest positive result on j= is Corollary 6 in [3].

A debate over the theoretical capabilities of formal methods in computer science has raged for more than two years now. The function of this paper is to summarize the key elements of this debate and to respond to important criticisms others have advanced by placing these issues within a broader context of philosophical considerations about the nature of hardware and of software and about the kinds of knowledge that we have the capacity to acquire concerning their performance.

This paper provides a review of Raymond Turner’s book Computational Artefacts. Towards a Philosophy of Computer Science. Focus is made on the definition of program correctness as the twofold problem of evaluating whether both the symbolic program and the physical implementation satisfy a set of specifications. The review stresses how these are not two separate problems. First, it is highlighted how formal proofs of correctness need to rely on the analysis of physical computational processes. Secondly, it is underlined (...) how software testing requires considering the formal relations holding between the specifications and the symbolic program. Such a mutual dependency between formal and empirical program verification methods is finally shown to influence the debate on the epistemological status of computer science. (shrink)

Vardi, M.Y., Verification of concurrent programs: the automata-theoretic framework, Annals of Pure and Applied Logic 51 79–98. We present an automata-theoretic framework to the verification of concurrent and nondeterministic programs. The basic idea is that to verify that a program P is correct one writes a program A that receives the computation of P as input and diverges only on incorrect computations of P. Now P is correct if and only if a program PA, obtained (...) by combining P and A, terminates. We formalize this idea in a framework of ω-automata with a recursive set of states. This unifies previous works on verification of fair termination and verification of temporal properties. (shrink)

This study developed an online career adaptability improvement program as part of the undergraduate curriculum to improve college students’ career adaptability and verify its effectiveness. This 13-week intervention program, developed using the Korea-Career Adaptability Scale, consists of three domains: knowledge and recognition of the self and work environment, self-directed coping related to career behavior, and environmental interaction for career decisions and adaptation. Two sub-studies were conducted to achieve the research objectives: Study 1 included developing and testing a pilot (...) program and Study 2 quantitatively analyzed the final program to test its effectiveness. In Study 1, preliminary program development and validity were verified, and in Study 2, the effectiveness of the final program was verified. As a strategy to achieve the research purpose, in Study 1, literature review and needs analysis, program design reflecting the results of the needs analysis, validity verification through Delphi survey, preliminary program implementation and evaluation, and the operation of the final program were performed. To test the effectiveness of the program in Study 2, a pre-posttest of career adaptability was conducted on experimental, comparison, and control groups using the non-equivalent group pretest–posttest design, followed by a program satisfaction survey. This study is meaningful in that it developed an online program to help college students improve career adaptability and identified its effectiveness. This study yielded two results. First, it successfully developed a career adaptability improvement program for undergraduate students, wherein the career development tasks, and the sub-factors of career adaptability were organically interlinked. Second, it verified the statistically significant differences in the career adaptability scores among the experimental, comparison, and control groups. The highest mean score was obtained by participants in the experimental group, followed by the comparison and the control group. (shrink)

Mathematical statements arising from program verification are believed to be much easier to deal with than statements coming from serious mathematics. At least this is true for “normal programming”.

This paper traces a relatively linear sequence of early research approaches to the formal verification of concurrent programs. It does so forwards and then backwards in time. After briefly outlining the context, the key insights from three distinct approaches from the 1970s are identified (Ashcroft/Manna, Ashcroft (solo) and Owicki). The main technical material in the paper focuses on a specific program taken from the last published of the three pieces of research (Susan Owicki’s): her own verification of (...) her _Findpos_ example is outlined followed by attempts at verifying the same example using the earlier approaches. Reconsidering the prior approaches on the basis of Owicki’s useful example illuminates similarities and differences between the proposals. Along the way, observations about interactions between researchers (and some “blind spots”) are noted. (shrink)

The purpose of the research is to determine the accuracy of the statements made by the mayors of Ecuador, and the inclusion of issues related to innovation and technology management, based on the fact-checking methodology. The research question is: Do the public statements of Ecuador’s mayors presented in local television news programs tend to be false? A quantitative methodology based on the Ecuador Chequea protocol was used. A sample of statements by mayors of eight cities was obtained and broadcasted between (...) February/20 and March/22. The statements are grouped in 10 axes, showing the correspondence between the functions determined in the law and the work they perform. Most of the statements refer to health in the face of Covid-19 control, followed by political issues, economy, public works and culture. The statements of the governors in this case are true, there is no contamination of fake news, the proximity helps direct accountability. (shrink)

This paper studies the complexity of behavior of multi-agent systems. Behavior properties are formulated using classical temporal logic languages and are checked with respect to the transition system induced by the definition of the multi-agent system. We establish various tight complexity bounds of the behavior properties under natural structural and semantic restrictions on agent programs and actions.

The main result of this paper belongs to the field of the comparative study of program verification methods as well as to the field called nonstandard logics of programs. We compare the program verifying powers of various well-known temporal logics of programs, one of which is the Intermittent Assertions Method, denoted as Bur. Bur is based on one of the simplest modal logics called S5 or sometime-logic. We will see that the minor change in this background modal (...) logic increases the program verifying power of Bur. The change can be described either technically as replacing the reflexive version of S5 with an irreflexive version, or intuitively as using the modality some-other-time instead of sometime. Some insights into the nature of computational induction and its variants are also obtained. (shrink)

Biró, B. and I. Sain, Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics, Annals of Pure and Applied Logic 63 201-225. We show that one can prove the partial correctness of more programs using Peano's axioms for the time frames of three-sorted time models than using only Presburger's axioms, that is it is useful to allow multiplication of time points at program verification and in dynamic and temporal logics. We organized (...) the paper as follows: 1. Preliminaries, 2. The main result, 3. Peano arithmetic with bounded multiplication, 4. Connections with temporal logics and dynamic logics, Acknowledgements, References. (shrink)

Almost all existing genetic programming systems deal with fitness evaluation solely by testing. In this paper, by contrast, we present an original approach that combines genetic programming with Hoare logic with the aid of model checking and finite state automata, henceby proposing a brand new verification-focused formal genetic programming system that makes it possible to evolve reliable programs with mathematicallyverified properties.

Introduction -- Algorithms, programs, procedures, and abstract automata -- Functioning of algorithms and automata, computation, and operations with algorithms and automata -- Basic postulates and axioms for algorithms -- Power of algorithms and classes of algorithms: comparison and evaluation -- Computing, accepting, and deciding modes of algorithms and programs -- Problems that people solve and related properties of algorithms -- Boundaries for algorithms and computation -- Software and hardware verification and testing -- Conclusion.

We present an initial and elementary investigation of the formal specification and mechanical verification of programs that interact with environments. We describe a formal, mechanically produced proof that a simple, real time control program keeps a vehicle on a straightline course in a variable crosswind. To formalize the specification we define a mathematical function which models the interaction of the program and its environment. We then state and prove two theorems about this function: the simulated vehicle never (...) gets farther than three units away from the intended course and homes to the course if the wind ever remains steady for at least four sampling intervals. (shrink)

A new approach for defining causality and such related notions as degree of responsibility, degrees of blame, and causal explanation. Causality plays a central role in the way people structure the world; we constantly seek causal explanations for our observations. But what does it even mean that an event C "actually caused" event E? The problem of defining actual causation goes beyond mere philosophical speculation. For example, in many legal arguments, it is precisely what needs to be established in order (...) to determine responsibility. The philosophy literature has been struggling with the problem of defining causality since Hume. In this book, Joseph Halpern explores actual causality, and such related notions as degree of responsibility, degree of blame, and causal explanation. The goal is to arrive at a definition of causality that matches our natural language usage and is helpful, for example, to a jury deciding a legal case, a programmer looking for the line of code that cause some software to fail, or an economist trying to determine whether austerity caused a subsequent depression. Halpern applies and expands an approach to causality that he and Judea Pearl developed, based on structural equations. He carefully formulates a definition of causality, and building on this, defines degree of responsibility, degree of blame, and causal explanation. He concludes by discussing how these ideas can be applied to such practical problems as accountability and program verification. Technical details are generally confined to the final section of each chapter and can be skipped by non-mathematical readers. (shrink)

An understanding of logic is essential to computer science. This book provides a highly accessible account of the logical basis required for reasoning about computer programs and applying logic in fields like artificial intelligence. The text contains extended examples, algorithms, and programs written in Standard ML and Prolog. No prior knowledge of either language is required. The book contains a clear account of classical first-order logic, one of the basic tools for program verification, as well as an introductory (...) survey of modal and temporal logics and possible world semantics. An introduction to intuitionistic logic as a basis for an important style of program specification is also featured in the book. (shrink)

The _logic of bunched implications_ (BI) can be seen as the free combination of _intuitionistic propositional logic_ (IPL) and _intuitionistic multiplicative linear logic_ (IMLL). We present here a base-extension semantics (B-eS) for BI in the spirit of Sandqvist’s B-eS for IPL, deferring an analysis of proof-theoretic validity (in the sense of Dummett and Prawitz) to another occasion. Essential to BI’s formulation in proof-theoretic terms is the concept of a ‘bunch’ of hypotheses, a notion familiar from relevance logic. Bunches amount to (...) trees whose internal vertices are labelled with either the IMLL or the IPL context-former and whose leaves are labelled with propositions or units for the context-formers. This structure presents significant technical challenges in setting up a base-extension semantics for BI. Our approach starts from the B-eS for IPL and the B-eS for IMLL and provides a systematic combination. Such a combination requires that base rules carry bunched structure, and so requires a more complex notion of derivability in a base and a correspondingly richer notion of support in a base. One reason why BI is a substructural logic of interest is that the ‘resource interpretation’ of its semantics, given in terms of sharing and separation and which gives rise to Separation Logic in the field of program verification, is quite distinct from the ‘number-of-uses’ interpretation of propositions in linear logic. This resource reading of BI provides useful intuitions in the formulation of its proof-theoretic semantics. We discuss a simple example of the use of the given B-eS in security modelling. (shrink)

Background: Classical computability and complexity theory analyze how costly a computation is in time or space, assuming inputs are already encoded as finite strings. The knowledge-representation tradition recognizes that representation choices constrain inference—most notably through the expressiveness–tractability tradeoff—but focuses on the complexity of querying a fixed representation, not on whether certain representational resources are necessary for a task to be expressible at all. Meanwhile, deep learning systems exhibit systematic failures on compositional and multi-object reasoning, symbolic systems face the classical symbol-grounding (...) problem, and neuro-symbolic architectures lack a formal account of which representational resources are required for which tasks. -/- Objectives: I aim to develop a computability-theoretic framework that classifies computational tasks by their minimal representational requirements—an axis orthogonal to time–space complexity—thereby providing formal criteria for determining when connectionist, symbolic, or neuro-symbolic architectures are representationally adequate, or provably inadequate, for a given task. -/- Methods: I introduce the Hierarchical Representational Machine (HRM), which stratifies representational resources into four layers: Structured Input Space (L1), grounded in Type-2 Theory of Effectivity; Equivalence and Measurement (L2), formalized via computable quotient spaces and representational measurement theory; Formal Symbolic Representation (L3), providing compositional syntax with effective derivation; and Admissibility Constraints (L4), supplying decidable meta-level filters for safety, legality, and verification. For each layer, I define necessity schemas that identify structural conditions on tasks—invariance, unbounded compositionality, and hard admissibility—under which that layer is provably required. I establish separation results via diagonal and undecidability arguments, and introduce the meta-problem HRM-Classify with the minimal requirement operator Req(T). -/- Results: The main results are: (i) three necessity schemas identifying when specific layers are unavoidable; (ii) separation theorems establishing strict gaps between layer-restricted solvability classes—{L1} ⊊ {L1,L2}, {L3} ⊊ {L1,L2,L3}, and {L1,L2,L3} ⊊ {L1,L2,L3,L4} under external-standard semantics—demonstrating that these layers correspond to genuine computability-theoretic distinctions even for constant-output tasks; and (iii) a solvability classification via Req(T) with worked examples spanning object recognition, program verification, and autonomous driving that illustrate the full layer hierarchy. -/- Conclusions: HRM provides a formal vocabulary for diagnosing representational insufficiency in AI systems: distribution-shift brittleness is identified as missing invariance structure, systematic compositional failures as insufficient symbolic resources, and constraint violations as absent admissibility gates. The framework serves as a principled pre-architectural analysis tool that determines minimal representational commitments before algorithm selection. Because HRM addresses representational feasibility rather than computational efficiency, it complements existing frameworks such as PAC/VC theory, knowledge compilation, and category-theoretic approaches, and is applicable wherever the question "what must be representable?" precedes "how hard is inference?". (shrink)

One might poetically muse that computers have the essence both of logic and machines. Through the case of the history of Separation Logic, we explore how this assertion is more than idle poetry. Separation Logic works because it merges the software engineer’s conceptual model of a program’s manipulation of computer memory with the logical model that interprets what sentences in the logic are true, and because it has a proof theory which aids in the crucial problem of scaling the (...) reasoning task. Scalability is a central problem, and some would even say the central problem, in appli- cations of logic in computer science. Separation Logic is an interesting case because of its widespread success in verification tools. For these two senses of model—the engineering/conceptual and the logical—to merge in a genuine sense, each must maintain their norms of use from their home disciplines. When this occurs, both the logic and engineering benefit greatly. Seeking this intersection of two different senses of model provides a strategy for how computer scientists and logicians may be successful. Furthermore, the history of Separation Logic for analysing programs provides a novel case for philosophers of science of how software engineers and computer scientists develop models and the components of such models. We provide three contributions: an exploration of the extent of models merging that is necessary for success in computer science; an introduction to the technical details of Separation Logic, which can be used for reasoning about other exhaustible resources; and an introduction to the problems, process, and results of computer scientists for those outside the field. (shrink)

Prominent experts present papers which discuss problems regarding this subject. Coverage includes case studies in the translation of logics for second-order and propositional dynamic logic; many-sorted algebras and equational logic; logical foundations of artificial intelligence along with a variety of methods that exist to encode information; program verification techniques such as Floyd-Hoare, intermittent assertion and temporal logic of programs.

We devise imperative programming languages for verified real number computation where real numbers are provided as abstract data types such that the users of the languages can express real number computation by considering real numbers as abstract mathematical entities. Unlike other common approaches toward real number computation, based on an algebraic model that lacks implementability or transcendental computation, or finite-precision approximation such as using double precision computation that lacks a formal foundation, our languages are devised based on computable analysis, a (...) foundation of rigorous computation over continuous data. Consequently, the users of the language can easily program real number computation and reason about the behaviours of their programs, relying on their mathematical knowledge of real numbers without worrying about artificial roundoff errors. As the languages are imperative, we adopt precondition–postcondition-style program specification and Hoare-style program verification methodologies. Consequently, the users of the language can easily program a computation over real numbers, specify the expected behaviour of the program, including termination, and prove the correctness of the specification. Furthermore, we suggest extending the languages with other interesting continuous data, such as matrices, continuous real functions, et cetera.Abstract taken directly from the thesis.E-mail: [email protected]: https://sewonpark.com/thesis. (shrink)

In this paper we study automated reasoning in the modal logic CPDLreg which is a combination of CPDL (Propositional Dynamic Logic with Converse) and REGc (Regular Grammar Logic with Converse). The logic CPDL is widely used in many areas, including program verification, theory of action and change, and knowledge representation. On the other hand, the logic REGc is applicable in reasoning about epistemic states and ontologies (via Description Logics). The modal logic CPDLreg can serve as a technical foundation (...) for reasoning about agency. Even very rich multi-agent logics can be embedded into CPDLreg via a suitable translation. Therefore, CPDLreg can serve as a test bed to implement and possibly verify new ideas without providing specific automated reasoning techniques for the logic in question. This process can to a large extent be automated. The idea of embedding various logics into CPDLreg is illustrated on a rather advanced logic TEAMLOGK designed to specify teamwork in multi-agent systems. Apart from defining informational and motivational attitudes of groups of agents, TEAMLOGK allows for grading agents' beliefs, goals and intentions. The current paper is a companion to our paper (Dunin-Kęplicz et al., 2010a). The main contribution are proofs of soundness and completeness of the tableau calculus for CPDLreg provided in (Dunin-Kęplicz et al., 2010a). (shrink)

This paper is concerned with techniques for identifying simple and quantified lattice points in 2SAT polytopes. 2SAT polytopes generalize the polyhedra corresponding to Boolean 2SAT formulas, Vertex-Packing and Network flow problems; they find wide application in the domains of Program verification and State-Space search . Our techniques are based on the symbolic elimination strategy called the Fourier-Motzkin elimination procedure and thus have the advantages of being extremely simple and incremental. We also provide a characterization of a 2SAT polytope (...) in terms of its extreme points and derive some interesting hardness results for associated optimization problems. Finally, we provide a brief discussion on the maximum size of a subdeterminant of the linear system representing a 2SAT polytope; this parameter plays a vital role in deriving analytical bounds on the size of the search space for checking whether the polyhedron includes a lattice point. (shrink)

In this dissertation, we construct a consistent, complete quotational logic G$\sb1$. We first develop a semantics, and then show the undecidability of circular quotation and anaphorism . Next, a complete axiom system is presented, and completeness theorems are shown for G$\sb1$. We show that definable truth exists in G$\sb1$. ;Later, we replace equality in G$\sb1$ with an equivalence relation. An axiom system and completeness theorems are provided for this equality-free version of G$\sb1$, which is useful in program verification. (...) ;Interpolation and definability are discussed in intensional and extensional contexts. We show that G$\sb1$ contains the complete first order theory of arithmetic by implicit definitional extension. ;The last chapter deals with representability and fixed points. Derived induction schemata are produced, and G$\sb1$ is shown to be a recursion theory. We give an example of how G$\sb1$ may be used to solve domain equations of Scott. (shrink)

We describe KAT-ML, an implementation of an interactive theorem prover for Kleene algebra with tests. The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. One can also use the system to reason about properties of simple imperative programs using schematic KAT. We explain how the system works and illustrate its use with some examples, including an extensive scheme equivalence proof.

The health of an intellectual ecosystem depends on its capacity to distinguish between original contributions and derivative reformulations. This paper introduces the CLEO Verification Protocol v1.0, a binary diagnostic tool designed to determine whether a conceptual framework is structurally derivative of a pioneer conceptual innovation. The protocol is grounded in the concept of Epistemic Immunity: the capacity of a sovereign research program to establish clear, objective boundaries between its own conceptual architecture and that of later, unacknowledged reproductions. Rather (...) than relying on proof of access, knowledge, or intent, the protocol operates on a set of formal, binary conceptual signatures that capture the constitutive core of the original innovation. This paper presents the logical structure of the protocol, its theoretical foundation in the concept of Epistemic Immunity, and its first field of application: the Evolutio Unfolding Theory (EUT). The case of Michael Levin's "Platonic Space" framework (2025) is presented as the first documented application of the protocol, demonstrating its capacity to discriminate between different degrees of structural reproduction while maintaining a binary, evidence-based standard. The protocol is offered as a permanent, objective instrument for the verification of conceptual lineage, and as a methodological contribution to the broader problem of conceptual attribution in science. (shrink)

Formal verification aims to prove whether models satisfy specifications, such as showing a program does what its designer intended. Formal verification is a promising approach that can be used to establish safety, security, and trustworthiness specifications of AI systems. However, to realize the potential societal benefits AI promise, we also need transdisciplinary approaches bridging the gamut from computer science and engineering, the broader sciences, as well as the arts, humanities, social sciences, law, business, and beyond to ensure (...) its development involves all perspectives and voices.My personal AI mission: To develop formal verification methods to help establish and assure the safe, secure, and trustworthy development and use of AI, especially in the context of safety-critical systems such as autonomous cyber-physical systems (CPS). (shrink)

Deductive verification provides a proof that, under the provided pre-conditions, each terminating execution of a given function satisfies the stated post-conditions. In general, pre- and post-conditions are expressed in a logical specification language and typically rely on theories including abstract definitions, axioms and lemmas. As they are written by humans, errors may be introduced into specifications. Some errors can be detected when the proof fails, but sometimes, they remain unnoticed due to misleading proofs: most of the program may (...) become dead code under the provided pre-conditions, or the proof may succeed because of inconsistencies in hypotheses and axioms. In this tool paper, we explore how to detect such unwanted situations by using deductive verification techniques and describe the smoke test mechanism in Frama-C/WP, a popular deductive verifier for C code. We show that, while the intuitive idea is simple, making it practical requires optimizations to scale up, and report on experiments with critical industrial code. Although our method is based on proof techniques, it is not complete and is similar to testing. In the end, can we ever be sure that our programs are proved well enough? (shrink)

Programming involves the construction of programs that meet their specifications. This draws in all the associated activities of programming such as testing, verification, and establishing correctness. And these are rule following activities.

The prelims comprise: Introduction Computer Science and Mathematics The Formal Verification Debate Abstraction in Computer Science Conclusion.

The verification of a sentence against a visual display in experimental conditions reveals a procedure that is driven solely by the properties of the linguistic input and not by the properties of the context (the set-up of the visual display) or extra-linguistic cognition (operations executed to obtain the truth value). This procedure, according to the Interface Transparency Thesis (ITT) (Lidz et al. in Nat Lang Semant 19(3):227–256, 2011), represents the meaning of an expression at the interface with the ‘conceptual-intentional’ (...) system (Chomsky in The minimalist program. MIT Press, Cambridge, 1995). My experiments provide support for the ITT by replicating in Polish and in Bulgarian the findings of Lidz et al. (Nat Lang Semant 19(3):227–256, 2011) for the English quantifier most. We also obtain new evidence that participants are prompted to switch between verification procedures by a change in the linguistic input (a different superlative quantifier entailed by most), but not by a change in the visual input. Thus, the motivation for the subconscious switch in procedures is not to maximize efficiency. Participants use the procedure associated with each quantifier, and in effect, the same display is verified differently depending on which information the visual system is instructed to use by the semantic representation of the sentence. (shrink)

The automatic verification of large parts of mathematics has been an aim of many mathematicians from Leibniz to Hilbert. While Gödel's first incompleteness theorem showed that no computer program could automatically prove certain true theorems in mathematics, the advent of electronic computers and sophisticated software means in practice there are many quite effective systems for automated reasoning that can be used for checking mathematical proofs. This book describes the use of a computer program to check the proofs (...) of several celebrated theorems in metamathematics including those of Gödel and Church-Rosser. The computer verification using the Boyer-Moore theorem prover yields precise and rigorous proofs of these difficult theorems. It also demonstrates the range and power of automated proof checking technology. The mechanization of metamathematics itself has important implications for automated reasoning, because metatheorems can be applied as labor-saving devices to simplify proof construction. (shrink)

The Zn helical identification program imposes the mode constraint k ≡ m (mod n) (diagonal sublattice Dn) on scalar field modes in the interior of rotating spacetimes with backward v-shift, and the constraint kz + m ≡ 0 (mod n) (anti-diagonal sublattice An) in the Chronotunnel Toroid with forward z-shift. Both sublattices have density 1/n in Z 2 . We provide a single unified treatment establishing three results that stand independently of the companion preprint series. (i) Exact algebraic decomposition. (...) Using the discrete Fourier representation of the sublattice indicator function, the renormalized stress-energy tensor in the method-of-images construction decomposes exactly as ⟨Tµν⟩ (n) ren = 1 n ⟨Tµν⟩ (1) ren + 1 n nX−1 j=1 T µν j , where T µν j are twisted image sums carrying the phase e 2πij(k−m)/n (or e 2πij(kz+m)/n for the antidiagonal case). This decomposition is exact and model-independent, and the 1/n prefactor of the direct term follows identically from the method-of-images structure of the two-point function. (ii) Unconditional leading-UV vanishing. For all j ̸≡ 0 (mod n), the leading UV contribution to the twisted image sums involves the polylogarithm Li−2(e iθ) evaluated at θ = 2πj/n. We prove that Li−2(e iθ) is purely imaginary for all θ ∈ (0, 2π), so Re Li−2(e iθ) -/- = 0 exactly. Consequently, in zeta-function regularization and at leading UV order, Re⟨Tµν⟩ (n) ren = (1/n) Re⟨Tµν⟩ (1) ren +O(β) with no hypothesis on the twisted sums. This is an unconditional result at leading UV order; whether subleading O(β) corrections are bounded or divergent near the horizon is identified as the central remaining open computation. (iii) Verification in the exactly solvable flat model. The flat helical Zn spacetime (Ref. [8]) provides a fully controlled, closed-form check: the method-of-images Green’s function there yields ⟨Tvv⟩ (n) ren ∼ C (n) /(r−rc,1) 4 with C (n) = C (1)/n exactly, confirming that the image-sum decomposition correctly tracks the coefficient of the near-horizon divergence, not merely its UV mode density. The three mathematical results above are self-contained. As an application to near-extremal supermassive Kerr (drawing on companion preprints), the 1/n suppression combined with geodesic blueshift suppression yields a residual stress-energy ∼ 10−230ρPl and a horizon destruction timescale ∼ 10300 yr, rendering the primary quantum mechanism for Hawking’s chronology protection conjecture inoperative on any cosmological timescale in this class of spacetime. (shrink)

In the theory of programming languages, type inference is the process of inferring the type of an expression automatically, often making use of information from the context in which the expression appears. Such mechanisms turn out to be extremely useful in the practice of interactive theorem proving, whereby users interact with a computational proof assistant to constructformal axiomatic derivations of mathematical theorems. This article explains some of the mechanisms for type inference used by the "Mathematical Components" project, which is working (...) towards a verification of the Feit-Thompson theorem. (shrink)

Motivated by the verification of programs with pointer variables, we introduce a temporal logic whose underlying assertion language is the quantifier-free fragment of separation logic and the temporal logic on the top of it is the standard linear-time temporal logic LTL. We analyze the complexity of various model-checking and satisfiability problems for, considering various fragments of separation logic, various classes of models, and the influence of fixing the initial memory state. We provide a complete picture based on these criteria. (...) Our main decidability result is pspace-completeness of the satisfiability problems on the record fragment and on a classical fragment allowing pointer arithmetic. -completeness or -completeness results are established for various problems by reducing standard problems for Minsky machines, and underline the tightness of our decidability results. (shrink)

From the Philosophies journal program, one of the main aims of the journal is to help establish a new unity in diversity in human knowledge, which would include both “Wissen” (i.e., “Wissenschaft”) and “sc¯ıre” (i.e., “science”). As is known, “Wissenshaft” (the pursuit of knowledge, learning, and scholarship) is a broader concept of knowledge than “science”, as it involves all kinds of knowledge,including philosophy, and not exclusively knowledge in the form of directly testable explanations and predictions. The broader notion of (...) scholarship incorporates an understanding and articulation of the role of the learner and the process of the growth of knowledge and its development, rather than only the final product and its verification and validation. In other words, it is a form of knowledge that is inclusive of both short-term and long-term perspectives; it is local and global, critical and hypothetical (speculative), breaking new ground. This new synthesis or rather re-connection of knowledge is expected to resonate with basic human value systems, including cultural values. Since knowledge tends to spontaneously fragment while it grows, we take existing diversity as a resource and a starting point for a new synthesis. The idea of broad, inclusive knowledge is in fact not so new. From the beginning, natural philosophy included all contemporary knowledge about nature. Newton was a natural philosopher, as were Bohr, Einstein, Prigogine, Weizsäcker, and Wheeler—to name but a few. Today, the unifying picture of the natural/physical world is sorely missing among the isolated silos of particular scientific domains, each with its own specific ontologies, methodologies, and epistemologies. From the profound need for connected and common knowledge, new trends towards synthesis have emerged in the last decades. One major theme is complexity, especially when applied to biology or medicine, which helps us to grasp the importance of connectedness between present-day disparate pieces of knowledge—frameworks, theories, approaches, etc. Related to this is the emergence of network science, which studies structures of nodes (actors) and edges as connections between them. This book is connecting work on contemporary natural philosophy and its connections with existing philosophies, sciences and other knowledge fields. (shrink)