Skip to main content
main-content

Über dieses Buch

This book constitutes the refereed proceedings of the International Symposium on Logical Foundations of Computer Science, LFCS 2020, held in Deerfield Beach, FL, USA, in January 2020. The 17 revised full papers were carefully reviewed and selected from 30 submissions. The scope of the Symposium is broad and includes 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.

Inhaltsverzeichnis

Frontmatter

Computability of Algebraic and Definable Closure

Abstract
We consider computability-theoretic aspects of the algebraic and definable closure operations for formulas. We show that for \(\varphi \) a Boolean combination of \(\varSigma _n\)-formulas and in a given computable structure, the set of parameters for which the closure of \(\varphi \) is finite is \(\varSigma ^0_{n+2}\), and the set of parameters for which the closure is a singleton is \(\varDelta ^0_{n+2}\). In addition, we construct examples witnessing that these bounds are tight.
Nathanael Ackerman, Cameron Freer, Rehana Patel

Observable Models

Abstract
Epistemic reading of Kripke models relies on a hidden assumption of common knowledge of the model which is too restrictive in epistemic contexts since agents may have different views of the situation. We explore possible worlds models in their full generality without common knowledge assumptions. Our starting point is a collection of possible worlds with accessibility relations “whatever is known in u is true in v.” We call such a structure an observable model since, contrary to the popular belief, it is not generally a Kripke model but rather an “observable section” of some Kripke model. We sketch a theory of observable models and argue that they bring a new conceptual clarity to epistemic modeling. In practical terms, observable models are as manageable as Kripke models and have advantages over the latter in representing (un)awareness and ignorance. Similar analysis applies to intuitionistic models.
Sergei Artemov

Countermodel Construction via Optimal Hypersequent Calculi for Non-normal Modal Logics

Abstract
We develop semantically-oriented calculi for the cube of non-normal modal logics and some deontic extensions. The calculi manipulate hypersequents and have a simple semantic interpretation. Their main feature is that they allow for direct countermodel extraction. Moreover they provide an optimal decision procedure for the respective logics. They also enjoy standard proof-theoretical properties, such as a syntactical proof of cut-admissibility.
Tiziano Dalmonte, Björn Lellmann, Nicola Olivetti, Elaine Pimentel

Completeness Theorems for First-Order Logic Analysed in Constructive Type Theory

Abstract
We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game semantics. As completeness with respect to standard model-theoretic semantics is not readily constructive, we analyse the assumptions necessary for particular syntax fragments and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.
Yannick Forster, Dominik Kirst, Dominik Wehr

On the Constructive Truth and Falsity in Peano Arithmetic

Abstract
Recently, Artemov [4] offered the notion of constructive truth and falsity in the spirit of Brouwer-Heyting-Kolmogorov semantics and its formalization, the Logic of Proofs. In this paper, we provide a complete description of constructive truth and falsity for Friedman’s constant fragment of Peano Arithmetic. For this purpose, we generalize the constructive falsity to n-constructive falsity where n is any positive natural number. We also establish similar classification results for constructive truth and n-constructive falsity of Friedman’s formulas. Then, we discuss ‘extremely’ independent sentences in the sense that they are classically true but neither constructively true nor n-constructive false for any n.
Hirohiko Kushida

Belief Expansion in Subset Models

Abstract
Subset models provide a new semantics for justifcation logic. The main idea of subset models is that evidence terms are interpreted as sets of possible worlds. A term then justifies a formula if that formula is true in each world of the interpretation of the term.
In this paper, we introduce a belief expansion operator for subset models. We study the main properties of the resulting logic as well as the differences to a previous (symbolic) approach to belief expansion in justification logic.
Eveline Lehmann, Thomas Studer

Finitism, Imperative Programs and Primitive Recursion

Abstract
The finitistic philosophy of mathematics, critical of referencing infinite totalities, has been associated from its inception with primitive recursion. That kinship was not initially substantiated, but is widely assumed, and is supported by Parson’s Theorem, which may be construed as equating finitistic reasoning with finitistic computing.
In support of identifying PR with finitism we build on the generic framework of [7] and articulate a finitistic theory of finite partial-structures, and a generic imperative programming language for modifying them, equally rooted in finitism. The theory is an abstract generalization of Primitive Recursive Arithmetic, and the programming language is a generic generalization of first-order recurrence (primitive recursion). We then prove an abstract form of Parson’s Theorem that links the two.
Daniel Leivant

Knowledge of Uncertain Worlds: Programming with Logical Constraints

Abstract
Programming with logic for sophisticated applications must deal with recursion and negation, which have created significant challenges in logic, leading to many different, conflicting semantics of rules. This paper describes a unified language, DA logic, for design and analysis logic, based on the unifying founded semantics and constraint semantics, that support the power and ease of programming with different intended semantics. The key idea is to provide meta-constraints, support the use of uncertain information in the form of either undefined values or possible combinations of values, and promote the use of knowledge units that can be instantiated by any new predicates, including predicates with additional arguments.
Yanhong A. Liu, Scott D. Stoller

A Globally Sound Analytic Calculus for Henkin Quantifiers

Abstract
This paper presents a methodology to construct globally sound but possibly locally unsound analytic calculi for partial theories of Henkin quantifiers. It is demonstrated that locally sound analytic calculi do not exist for any reasonable fragment of the full theory of Henkin quantifiers. This is due to the combination of strong and weak quantifier inferences in one quantifier rule.
Matthias Baaz, Anela Lolic

Feedback Hyperjump

Abstract
Feedback is oracle computability when the oracle consists exactly of the con- and divergence information about computability relative to that same oracle. Here we study the feedback version of the hyperjump.
Robert S. Lubarsky

Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents

Abstract
This paper employs the linear nested sequent framework to design a new cut-free calculus (\(\mathsf {LNIF}\)) for intuitionistic fuzzy logic—the first-order Gödel logic characterized by linear relational frames with constant domains. Linear nested sequents—which are nested sequents restricted to linear structures—prove to be a well-suited proof-theoretic formalism for intuitionistic fuzzy logic. We show that the calculus \(\mathsf {LNIF}\) possesses highly desirable proof-theoretic properties such as invertibility of all rules, admissibility of structural rules, and syntactic cut-elimination.
Tim Lyon

On Deriving Nested Calculi for Intuitionistic Logics from Semantic Systems

Abstract
This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable proof-theoretic properties from its associated labelled calculus.
Tim Lyon

Parameterised Complexity of Abduction in Schaefer’s Framework

Abstract
Abductive reasoning is a non-monotonic formalism stemming from the work of Peirce. It describes the process of deriving the most plausible explanations of known facts. Considering the positive version asking for sets of variables as explanations, we study, besides asking for existence of the set of explanations, two explanation size limited variants of this reasoning problem (less than or equal to, and equal to). In this paper, we present a thorough two-dimensional classification of these problems. The first dimension is regarding the parameterised complexity under a wealth of different parameterisations. The second dimension spans through all possible Boolean fragments of these problems in Schaefer’s constraint satisfaction framework with co-clones (STOC 1978). Thereby, we almost complete the parameterised picture started by Fellows et al. (AAAI 2012), partially building on results of Nordh and Zanuttini (Artif. Intell. 2008). In this process, we outline a fine-grained analysis of the inherent parameterised intractability of these problems and pinpoint their FPT parts. As the standard algebraic approach is not applicable to our problems, we develop an alternative method that makes the algebraic tools partially available again.
Yasir Mahmood, Arne Meier, Johannes Schmidt

Tracking Computability of GPAC-Generable Functions

Abstract
Analog computation attempts to capture any type of computation, that can be realized by any type of physical system or physical process, including but not limited to computation over continuous measurable quantities. A pioneering model is the General Purpose Analog Computer (GPAC), initially presented by Shannon in 1941. The GPAC is capable of manipulating real-valued data streams; however, it has been shown to be strictly less powerful than other models of computation on the reals, such as computable analysis.
In previous work, we proposed an extension of the Shannon GPAC, denoted LGPAC, designed to overcome its limitations. Not only is the LGPAC model capable of expressing computation over general data spaces \(\mathcal {X}\), it also directly incorporates approximating computations by means of a limit module. In this paper, we compare the LGPAC with a digital model of computation based on effective representations (tracking computability). We establish general conditions under which LGPAC-generable functions are tracking computable.
Diogo Poças, Jeffery Zucker

Modal Type Theory Based on the Intuitionistic Modal Logic

Abstract
The modal intuitionistic epistemic logic \(\mathbf{IEL}^{-}\) was proposed by Artemov and Protopopescu as the intuitionistic version of belief logic. We construct the modal lambda calculus which is Curry-Howard isomorphic to \(\mathbf{IEL}^{-}\) as the type-theoretical representation of applicative computation widely known in functional programming.
Daniel Rogozin

Lifting Recursive Counterexamples to Higher-Order Arithmetic

Abstract
In classical computability theory, a recursive counterexample to a theorem shows that the latter does not hold when restricted to computable objects. These counterexamples are highly useful in the Reverse Mathematics program, where the aim of the latter is to determine the minimal axioms needed to prove a given theorem of ordinary mathematics. Indeed, recursive counterexamples often (help) establish the ‘reverse’ implication in the typical equivalence between said minimal axioms and the theorem at hand. The aforementioned is generally formulated in the language of second-order arithmetic and we show in this paper that recursive counterexamples are readily modified to provide similar implications in higher-order arithmetic. For instance, the higher-order analogue of ‘sequence’ is the topological notion of ‘net’, also known as ‘Moore-Smith sequence’. Our results on metric spaces suggest that the latter can only be reasonably studied in weak systems via representations (aka codes) in the language of second-order arithmetic.
Sam Sanders

On the Tender Line Separating Generalizations and Boundary-Case Exceptions for the Second Incompleteness Theorem Under Semantic Tableaux Deduction

Abstract
Our previous research has studied the semantic tableaux deductive methodology, of Fitting and Smullyan, and observed that it permits boundary-case exceptions to the Second Incompleteness Theorem, when multiplication is viewed as a 3-way relation (rather than as a total function). It is known that tableaux methodologies do prove a schema of theorems, verifying all instances of the Law of the Excluded Middle. But yet we show that if one promotes this schema of theorems into formalized logical axioms, then the meaning of the pronoun “I” in our self-referencing engine changes, and our partial evasions of the Second Incompleteness Theorem come to a complete halt.
Dan E. Willard

Backmatter

Weitere Informationen

Premium Partner

    Bildnachweise