This volume stems from the International Symposium on Logical Foundations of Computer Science (LFCS’22), held online, 10–13 January 2022. Subsequent to that meeting, some of the speakers were invited to contribute to this volume. The LFCS’22 Steering Committee consisted of Anil Nerode (Ithaca, NY, USA; General Chair), Samuel Buss (San Diego, CA, USA), Stephen Cook (Toronto), Dirk van Dalen (Utrecht), Yuri Matiyasevich (St. Petersburg), Andre Scedrov (Philadelphia, PA) and Dana Scott (Pittsburgh, PA/Berkeley, CA, USA). LFCS’22 topics of interest included, but were not limited to, constructive mathematics and type theory; homotopy-type theory; logic, automata and automatic structures; computability and randomness; logical foundations of programming; logical aspects of computational complexity; parameterized complexity; logic programming and constraints; automated deduction and interactive theorem proving; logical methods in protocol and program verification; logical methods in program specification and extraction; domain theory logics; logical foundations of database theory; equational logic and term rewriting; lambda and combinatory calculi; categorical logic and topological semantics; linear logic; epistemic and temporal logics; intelligent and multiple-agent system logics; logics of proof and justification; non-monotonic reasoning; logic in game theory and social software; logic of hybrid systems; distributed system logics; mathematical fuzzy logic; system design logics; and other logics in computer science.

The origins of this volume are with The International Symposium on Logical Foundations of Computer Science (LFCS’16), held in Deerfield Beach, Florida, January 4 – 7, 2016. Afterwards, some speakers were invited to contribute to a volume, and the invitation was extended more generally as well. LFCS’16 Steering Committee comprised Anil Nerode, (Ithaca, NY, General Chair); Stephen Cook (Toronto); Dirk van Dalen (Utrecht); Yuri Matiyasevich (St. Petersburg); Alan Robinson (Syracuse, NY); Gerald Sacks (Cambridge, MA); Dana Scott, (Pittsburgh, PA – Berkeley, CA). LFCS’16 topics of interest included, but were not limited to: constructive mathematics and type theory; homotopy type theory; logic, automata, and automatic structures; computability and randomness; logical foundations of programming; logical aspects of computational complexity; parameterized complexity; logic programming and constraints; automated deduction and interactive theorem proving; logical methods in protocol and program verification; logical methods in program specification and extraction; domain theory logics; logical foundations of database theory; equational logic and term rewriting; lambda and combinatory calculi; categorical logic and topological semantics; linear logic; epistemic and temporal logics; intelligent and multiple-agent system logics; logics of proof and justification; non-monotonic reasoning; logic in game theory and social software; logic of hybrid systems; distributed system logics; mathematical fuzzy logic; system design logics; other logics in computer science.

Hybrid systems are heterogenous dynamical systems characterized by interacting continuous and discrete dynamics. Such mathematical models have proved fruitful in a great diversity of engineering applications, including air-traffic control, automated manufacturing, and chemical process control. The high-profile and safety-critical nature of the application areas has fostered a large and growing body of work on formal methods for hybrid systems: mathematical logics, computational models and methods, and computer-aided reasoning tools supporting the formal specification and verification of performance requirements for hybrid systems, and the design and synthesis of control programs for hybrid systems that are provably correct with respect to formal specifications. This paper offers synthetic overview of, and original contributions to, the use of logics and formal methods in the analysis of hybrid systems.

For many military and civilian large-scale, real-world systems of interest, data are first acquired asynchronously, i.e., at irregular intervals of time, at geographically-dispersed sites, processed utilizing decision-making algorithms, and the processed data then disseminated to other appropriate sites. The term real-world refers to systems under computer control that relate to everyday life and are beneficial to the society in the large. The traditional approach to such problems consists of designing a central entity which collects all data, executes a decision-making algorithm sequentially to yield the decisions, and propagates the decisions to the respective sites. Centralized decision-making algorithms are slow and highly vulnerable to natural and artificial catastrophes. Recent literature includes successful asynchronous, distributed, decision-making algorithm designs wherein the local decision making at every site replaces the centralized decision making to achieve faster response, higher reliability, and greater accuracy of the decisions. Two key issues include (1) the lack of an approach to synthesize asynchronous, distributed, decision-making algorithms, for any given problem, and (2) the absence of a comparative analysis of the quality of their decisions. This paper proposes MFAD, a Mathematical Framework for Asynchronous, Distributed Systems, that permits the description of centralized decision-making algorithms and facilities the synthesis of distributed decision-making algorithms. MFAD is based on the Kohn-Nerode distributed hybrid control paradigm.

For many military and civilian large-scale, real-world systems of interest, data are first acquired asynchronously, i.e. at irregular intervals of time, at geographically-dispersed sites, processed utilizing decision-making algorithms, and the processed data then disseminated to other appropriate sites. The term real-world refers to systems under computer control that relate to everyday life and are beneficial to the society in the large. The traditional approach to such problems consists of designing a central entity which collects all data, executes a decision making algorithm sequentially to yield the decisions, and propagates the decisions to the respective sites. Centralized decision making algorithms are slow and highly vulnerable to natural and artificial catastrophes. This paper proposes MFAD, a Mathematical Framework for Asynchronous, Distributed Systems, that permits the description of centralized decision-making algorithms and facilities the synthesis of distributed decision-making algorithms. MFAD is based on the Kohn-Nerode distributed hybrid control paradigm. It has been a belief that since the centralized control gathers every necessary data from all entities in the system and utilizes them to compute the decisions, the decisions may be "globally" optimal. In truth, however, as the frequency of the sensor data increases and the environment gets larger, dynamic, and more complex, the decisions are called into question.

In this paper we introduce effectiveness into model theory of intuitionistic logic. The main result shows that any computable theory T of intuitionistic predicate logic has a Kripke model with decidable forcing such that for any sentence φ, φ is forced in the model if and only if φ is intuitionistically deducible from T.

We introduce effectiveness considerations into model theory of intuitionistic logic. We investigate effectiveness of completeness (by Kripke) results for intermediate logics such as intuitionistic logic, classical logic, constant domain logic, directed frames logic, and Dummett's logic.

Normal default logic, the fragment of default logic obtained by restricting defaults to rules of the form α:Mβ/β, is the most important and widely studied part of default logic. In [20], we proved a basis theorem for extensions of recursive propositi

Annotated logics were proposed by Subrahmanian as a unified paradigm for representing a wide variety of reasoning tasks including reasoning with uncertainty within a single theoretical framework. Subsequently, Marek, Nerode and Remmel have shown how to provide nonmonotonic extensions of arbitrary languages through their notion of a nonmonotonic rule systems. The primary aim of this paper is to define annotated nonmonotonic rule systems which merge these two frameworks into a general purpose nonmonotonic reasoning framework over arbitrary multiple-valued logics. We then show how Reiter's normal default theories may be generalized to the framework of annotated nonmonotonic rule systems.

In this paper we consider the complexity of the existence problem for explanations and for minimal explanations for abductive frameworks based on finite predicate programs. We find that although, in general, the problem is very complex, there are classes of frameworks for which the problem is much simpler.

The content of existence theorems in the calculus of variations has been explored and an effective treatment of semi-continuity has been achieved. An algorithm has been developed which captures the natural algorithmic content of the notion of a semi-continuous function and this is used to obtain an effective version of the “chattering lemma” of control theory and ordinary differential equations. This lemma reveals the main computational content of the theory of relaxed optimal control.

In this paper, we study the lower semilattice of NP-subspaces of both the standard polynomial time representation and the tally polynomial time representation of a countably infinite dimensional vector space V∞ over a finite field F. We show that for both the standard and tally representation of V∞, there exists polynomial time subspaces U and W such that U + V is not recursive. We also study the NP analogues of simple and maximal subspaces. We show that the existence of P-simple and NP-maximal subspaces is oracle dependent in both the tally and standard representations of V∞. This contrasts with the case of sets, where the existence of NP-simple sets is oracle dependent but NP-maximal sets do not exist. We also extend many results of Nerode and Remmel (1990) concerning the relationship of P bases and NP-subspaces in the tally representation of V∞ to the standard representation of V∞.

Nerode et al. [ 131 showed that a correct concurrent program can be viewed as a winning strategy in a suitably defined two player game played between the Programmer and the Computer in which the program specification is defined by the rules of the game together with the winning condition. This gives rise to the question as to whether there are useful algorithms to extract (provably) winning strategies in these games, which then yield (provably correct) concurrent programs. Now these games can be described in Rabin’s S2S, the monadic second-order theory of two successors. Decision procedures for the latter show that such algorithms exist. But past available decision methods were too cumbersome to use, even in simple cases. Successively simpler game-based decision procedures for S2S were provided by [5,19,20]. In 1993, based on these papers, McNaughton [8] introduced a class of two player infinite games which are played on a finite graph and have an especially lucid decision procedure for extraction of winning strategies. The games considered in [ 131 can be viewed as a slight variant of Bi.ichi-Landweber games [2]. We give clean algorithms for the equivalence of McNaughton games and Bi.ichi-Landweber games. This allows the McNaughton algorithm to be used to extract (provably) winning strategies, and therefore (verifiably correct) concurrent programs via the Nerode-Yakbnis-Yakhnis paradigm.

The declarative semantics of nonmonotonic logic programming has largely been based on propositional programs. However, the ground instantiation of a logic program may be very large, and likewise, a ground stable model may also be very large. We develop a non-ground semantic theory for non-monotonic logic programming. Its principal advantage is that stable models and well-founded models can be represented as sets of atoms, rather than as sets of ground atoms. A set SI of atoms may be viewed as a compact representation of the Herbrand interpretation consisting of all ground instances of atoms in SI. We develop generalizations of the stable and well-founded semantics based on such non-ground interpretations SI. The key notions for our theory are those of covers and anticovers. A cover as well as its anticover are sets of substitutions — non-ground in general — representing all substitutions obtained by ground instantiating some substitution in the (anti)cover, with the additional requirement that each ground substitution is represented either by the cover or by the anticover, but not by both. We develop methods for computing anticovers for a given cover, show that membership in so-called optimal covers is decidable, and investigate the complexity in the Datalog case.

Unlike sets of definite Horn clauses, logic programs with disjunctions of atoms in clause heads are often interpreted in terms of minimal models. It is also well known that the minimal models of logic programs are closely related to the so-called stable models of logic programs with nonmonotonic negation in clause bodies, as well as to circumscription. Methods to compute minimal models of logic programs are becoming increasingly important as an intermediate step in the computation of structures associated with nonmonotonic logic programs. However, to date, all these techniques have been restricted to the case of propositional logic programs which means that an ordinary disjunctive logic program must be “grounded out” prior to computation. Grounding out in this manner leads to a combinatorial explosion in the number of clauses, and hence, is unacceptable. In this paper, we show how, given any method M which correctly computes the set of minimal models of a propositional logic program, we can develop a strategy to compute truth in a minimal model of a disjunctive logic program P. The novel feature of our method is that it works on an “instantiate-by-need” basis, and thus avoids unnecessary grounding.

Deductive databases that interact with, and are accessed by, reasoning agents in the real world (such as logic controllers in automated manufacturing, weapons guidance systems, aircraft landing systems, land-vehicle maneuvering systems, and air-traffic control systems) must have the ability to deal with multiple modes of reasoning. Specifically, the types of reasoning we are concerned with include, among others, reasoning about time, reasoning about quantitative relationships that may be expressed in the form of differential equations or optimization problems, and reasoning about numeric modes of uncertainty about the domain which the database seeks to describe. Such databases may need to handle diverse forms of data structures, and frequently they may require use of the assumption-based nonmonotonic representation of knowledge. A hybrid knowledge base is a theoretical framework capturing all the above modes of reasoning. The theory tightly unifies the constraint logic programming scheme of Jaffar and Lassez (1987), the generalized annotated logic programming theory of Kifer and Subrahmanian (1989), and the stable model semantics of Gelfond and Lifschitz (1988). New techniques are introduced which extend both the work on annotated logic programming and the stable model semantics.

Existing and past generations of Prolog compilers have left deduction to run-time and this may account for the poor run-time performance of existing Prolog systems. Our work tries to minimize run-time deduction by shifting the deductive process to compile-time. In addition, we offer an alternative inferencing procedure based on translating logic to mixed integer programming. This makes available for research and implementation in deductive databases, all the theorems, algorithms, and software packages developed by the operations research community over the past 50 years. The method keeps the same query language as for disjunctive deductive databases, only the inferencing procedure changes. The language is purely declarative, independent of the order of rules in the program, and independent of the order in which literals occur in clause bodies. The technique avoids Prolog's problem of infinite looping. It saves run-time by doing primary inferencing at compile-time. Furthermore, it is incremental in nature. The first half of this article translates disjunctive clauses, integrity constraints, and database facts into Boolean equations, and develops procedures to use mixed integer programming methods to compute equations, and develops procedures to use mixed integer programming methods to compute equations, and develops procedures to use mixed integer programming methods to compute equations, and develops procedures to use mixed integer programming methods to compute —least models of definite deductive databases, and —minimal models and the Generalized Closed World Assumption of disjunctive databases.

Normal default logic, the fragment of default logic obtained by restricting defaults to rules to the form /spl alpha/:M/spl beta///spl beta/. is the most important and widely studied part of default logic. In Annals of Pure and Applied Logic, vol. 67, pp. 269-324 (1994), we proved a basis theorem for extensions of recursive propositional logic normal default theories and hence for finite predicate logic normal default theories, i.e. we proved that every recursive propositional normal default theory possesses an extension which is recursively enumerable (r.e.) in 0'. In this paper, we show that this bound is tight. Specifically, we show that for every r.e. set A and every B which is r.e. in A, there is a recursive normal default theorywith a unique extension which is Turing-equivalent to A/spl oplus/B. A similar result holds for finite predicate logic normal default theories.

Though circumscription was introduced by McCarthy over a decade ago, there has been relatively little work on algorithms for computing circumscriptive databases. In this paper, we develop algorithms to compute the preferred models of circumscriptive databases at compile-time using mixed integer linear programming techniques. Two advantages of this (bottom-up) approach are that it makes efficient re-use of previous computations and it provides much faster run-time performance. Some other advantages of using linear programming to automate deduction at compile time are that its re-optimization facilities elegantly accommodate database updates and also that it leads to a completely declarative formulation in which ordering of rules and literals in rule bodies plays no real role. Finally, we plan to use a standard relational database system as our run-time environment; this should yield relatively fast run-time processing, and provide a more expressive query language in which aggregates and the like can be expressed easily.

Hybrid systems are interacting systems of digital automata and continuous plants subject to disturbances. The digital automata are used to force the state trajectory of the continuous plant to obey a performance specification. For the basic concepts and notation for hybrid systems, see Kohn and Nerode (1993), and other papers in the same volume. Here we introduce tools for analyzing enforcing viability of all possible plant state trajectories of a hybrid system by suitable choices of finite state control automata. Thus, the performance specification considered here is that the state of the plant remain in a prescribed viability set of states at all times (Aubin, 1991). The tools introduced are local viability graphs and viability graphs for hybrid systems. We construct control automata which guarantee viability as the fixpoints of certain operators on graphs. When control and state spaces are compact, the viability set is closed, and a non-empty closed subset of a viability graph is given with a sturdiness property, one can extract finite state automata guaranteeing viable trajectories. This paper is a sequel to Kohn and Nerode (1993), especially Appendix II.

Though the declarative semantics of both explicit and nonmonotonic negation in logic programs has been studied extensively, relatively little work has been done on computation and implementation of these semantics. In this paper, we study three different approaches to computing stable models of logic programs based on mixed integer linear programming methods for automated deduction introduced by R. Jeroslow. We subsequently discuss the relative efficiency of these algorithms. The results of experiments with a prototype compiler implemented by us tend to confirm our theoretical discussion. In contrast to resolution, the mixed integer programming methodology is both fully declarative and handles reuse of old computations gracefully. We also introduce, compare, implement, and experiment with linear constraints corresponding to four semantics for “explicit” negation in logic programs: the four-valued annotated semantics [Blair and Subrahmanian 1989], the Gelfond-Lifschitz semantics [1990], the over-determined models [Grant and Subrahmanian 1989], the Gelfond-Lifschitz semantics [1990], the over-determined models [Grant and Subrahmanian 1990], and the classical logic semantics. Gelfond and Lifschitz[1990] argue for simultaneous use of two modes of negation in logic programs, “classical” and “nonmonotonic,” so we give algorithms for computing “answer sets” for such logic programs too.

The semantics for nonmonotonic rule systems are investigated. The notion of nonmonotonic formal systems is then introduced. Examples are given, along with applications of logic, logic programming, and common-sense reasoning.>

An investigation is made of a logical framework for programming languages which treats requirements on computation resources as part of the formal program specification. Resource bounds are explicit in the syntax of all programs. In a programming language based on this approach, compliance of a program with imposed resource bounds would be assured by verifying the syntactic correctness using a compiler with a static type checking feature. The principal innovation is the introduction of systems of logical inference, called polynomially graded logics. These logics make resource bounds part of every proposition and every deduction. The sample calculus presented is a restriction of Godel's system T to polynomial time resources. It is proved that the numerical functions representable in this calculus are exactly the PTIME functions.>

Recursive equivalence types are an effective or recursive analogue of cardinal numbers. They were introduced by Dekker in the early 1950's. The richness of various theories related to the recursive equivalence types is demonstrated in this paper by showing that the theory of any countable relational structure can be embedded in or interpreted in these theories. A more complete summary is presented in the last paragraph of this section. Let E = {0,1, 2, …} be the natural numbers. If α ⊆ E, β ⊆ E, and there is a 1-1 partial recursive function f such that the image under f of α is β, α and β are called recursively equivalent (see [3]). The recursive equivalence type or RET of α, denoted 〈α〉, is the class of all β recursively equivalent to α. Addition of RETs is defined by 〈α〉 + 〈β〉 = 〈{2x ∣ x ∈ α} ∪ 〈{2x + 1 ∣ x ∈ β}〉. The partial ordering ≤ is defined on the RETs by A ≤ B iff (EC)(A + C = B). An RET, X, is called an isol if X ≠ X + 1 or, equivalently, if no representative of X is recursively equivalent to a proper subset of itself. The isols are thus the recursive analogue of the Dedekind-finite cardinals.