Axiomatic Synthesis of Computer Programs and Computability Theorems

The recently initiated approach called computability logic is a formal theory of interactive computation. See a comprehensive online source on the subject at http://www.cis.upenn.edu/~giorgi/cl.html . The present paper contains a soundness and completeness proof for the deductive system CL3 which axiomatizes the most basic first-order fragment of computability logic called the finite-depth, elementary-base fragment. Among the potential application areas for this result are th...

This book explores an alternative to the current dominant paradigm where a discrete computer model is constructed as an attempt to approximate some continuum theory. We focus on a class of discrete computer models that are based on simple deterministic rules and finite state arithmetic. Such models are highly compatible with the operational parameters of the real world computer on which they are executed and hence their validation can be associated with the allowable computat...

My research goal is to employ a parser generation algorithm based on the Earley parsing algorithm to the evaluation and compilation of queries to logic programs, especially to deductive databases. By means of partial deduction, from a query to a logic program a parameterized automaton is to be generated that models the evaluation of this query. This automaton can be compiled to executable code; thus we expect a speedup in runtime of query evaluation. An extended abstract/ ful...

We present the first class of mathematically rigorous, general, fully self-referential, self-improving, optimally efficient problem solvers. Inspired by Kurt Goedel's celebrated self-referential formulas (1931), such a problem solver rewrites any part of its own code as soon as it has found a proof that the rewrite is useful, where the problem-dependent utility function and the hardware and the entire initial code are described by axioms encoded in an initial proof searcher w...

We present a unified theory for formal mathematical systems including recursive systems closely related to formal grammars, including the predicate calculus as well as a formal induction principle. We introduce recursive systems generating the recursively enumerable relations between lists of terms, the basic objects under consideration. A recursive system consists of axioms, which are special quantifier-free positive horn formulas, and of specific rules of inference. Its ext...

Computers have already changed the way that humans do mathematics: they enable us to compute efficiently. But will they soon be helping us to reason? And will they one day start reasoning themselves? We give an overview of recent developments in neural networks, computer theorem provers and large language models.

Recently proposed models which learn to write computer programs from data use either input/output examples or rich execution traces. Instead, we argue that a novel alternative is to use a glass-box loss function, given as a program itself that can be directly inspected. Glass-box optimization covers a wide range of problems, from computing the greatest common divisor of two integers, to learning-to-learn problems. In this paper, we present an intelligent search system which...

This talk describes how a combination of symbolic computation techniques with first-order theorem proving can be used for solving some challenges of automating program analysis, in particular for generating and proving properties about the logically complex parts of software. The talk will first present how computer algebra methods, such as Groebner basis computation, quantifier elimination and algebraic recurrence solving, help us in inferring properties of program loops wit...

This introduction begins with a section on fundamental notions of mathematical logic, including propositional logic, predicate or first-order logic, completeness, compactness, the L\"owenheim-Skolem theorem, Craig interpolation, Beth's definability theorem and Herbrand's theorem. It continues with a section on G\"odel's incompleteness theorems, which includes a discussion of first-order arithmetic and primitive recursive functions. This is followed by three sections that are ...

This article presents an overview of applications of logic programming, classifying them based on the abstractions and implementations of logic languages that support the applications. The three key abstractions are join, recursion, and constraint. Their essential implementations are for-loops, fixed points, and backtracking, respectively. The corresponding kinds of applications are database queries, inductive analysis, and combinatorial search, respectively. We also discuss ...