WoLLIC 2023 Program

Traditional epistemic and doxastic logics cannot deal with inconsistent beliefs nor do they represent the evidence an agent possesses. So-called ‘evidence logics’ have been introduced to deal with both of those issues. The semantics of these logics are based on neighbourhood or hypergraph frames. The neighbourhoods of a world represent the basic evidence available to an agent. On one view, beliefs supported by evidence are propositions derived from all maximally consistent collections evidence. An alternative concept of beliefs takes them to be propositions derivable from consistent partitions of one’s inconsistent evidence; this is known as Schotch-Jennings Forcing. This paper develops a modal logic based on the hypergraph semantics to represent Schotch-Jennings Forcing. The modal language includes an operator U(φ1,...,φn;ψ) which is similar to one introduced in Instantial Neighbourhood Logic. It is of variable arity and the input formulas are enjoy distinct roles. The U operator expresses that all evidence at a particular world that supports ψ can be supported by at least one of the φis. U can then be used to express that all the evidence available can be unified by the finite set of formulas φ1,...,φn if ψ is taken to be ⊺. Future developments will then use that semantics as the basis for a doxastic logic akin to evidence logics.

We discuss two two-layered logics formalising reasoning with paraconsistent probabilities that combine the Łukasiewicz [0,1]-valued logic with Baaz △ operator and the Belnap–Dunn logic. The first logic Pr Ł2 △ (introduced in [7]) formalises a ‘two-valued’ approach where each event ϕ has independent positive and negative measures that stand for, respectively, the likelihoods of ϕ and ¬ϕ. The second logic 4Pr Ł△ that we introduce here corresponds to ‘four-valued’ probabilities. There, ϕ is equipped with four measures standing for pure belief, pure disbelief, conflict and uncertainty of an agent in ϕ.

We construct faithful embeddings of 4Pr Ł△ and Pr Ł2 △ into one another and axiomatise 4Pr Ł△ using a Hilbert-style calculus. We also establish the decidability of both logics and provide complexity evaluations for them using an expansion of the constraint tableaux calculus for Ł.

We define a new relatively simple Skolemization method called atomic Skolemization which allows for a non-elementarily bounded speed-up of cut-free LK-proofs and resolution proofs w.r.t. the standard Skolemization and Andrews Skolemization.

In this paper, the notion of structural completeness is explored in the context of a generalized class of superintuitionistic logics involving also systems that are not closed under uniform substitution. We just require that each logic must be closed under D-substitutions assigning to atomic formulas only ∨-free formulas. For these systems we introduce four different notions of structural completeness and study how they are related. We focus on superintuitionistic inquisitive logics that validate a schema called Split and have the disjunction property. In these logics disjunction can be interpreted in the sense of inquisitive semantics as a question forming operator. It is shown that a logic is structurally complete with respect to D-substitutions if and only if it includes the weakest superintuitionistic inquisitive logic. Various consequences of this result are explored. For example, it is shown that every superintuitionistic inquisitive logic can be characterized by a Kripke model built up from D-substitutions. Additionally, we resolve a conjecture concerning superintuitionistic inquisitive logics due to Miglioli et al.

Combining relevant and classical modal logic is an approach to overcoming the logical omniscience problem and related issues that goes back at least to Levesque’s well known work in the 1980s. The present authors have recently introduced a variant of Levesque’s framework where explicit beliefs concerning conditional propositions can be formalized. However, our framework did not offer a formalization of implicit belief in addition to explicit belief. In this paper we provide such a formalization. Our main technical result is a modular completeness theorem.

Aleatoric propositions are a generalisation of Boolean propo- sitions, that are intrinsically probabilistic, or determined by the toss of a (biased) coin. Rather than let propositions take a true/false valuation, we assume they act as a biased coin, that will sometimes land heads (true), and sometimes land tails (false). Complex propositions then cor- respond to a conditional series of tosses of these coins. We extend the syntax and semantics for Aleatoric Logic to include a novel fixed-point operator that is able to represent a weak form of iteration. We examine the expressivity of the of the language, showing a correspondence to the rational functions over (0,1).

Expectation Maximisation (EM) and Latent Dirichlet Allocation (LDA) are two frequently used inference algorithms, for finding an appropriate mixture of latent variables, and for finding an allocation of topics for a collection of documents. A recent insight in probabilistic learning is that Jeffrey’s update rule gives a decrease of Kullback-Leibler divergence. Its logic is error correction. It is shown that this same rule and divergence decrease logic is at the heart of EM and LDA, ensuring that successive iterations are decreasingly wrong.

This paper presents a justification counterpart for dyadic deontic logic, which is often argued to be better than Standard Deontic Logic at representing conditional and contrary-to-duty obligations, such as those exemplified by the notorious Chisholm’s puzzle. We consider the alethic-deontic system (E) and present the explicit version of this system (JE) by replacing the alethic Box-modality with proof terms and the dyadic deontic Circ-modality with justification terms. The explicit representation of strong factual detachment (SFD) is given and finally soundness and completeness of the system (JE) with respect to basic models and preference models is established.

Qualitative Choice Logic (QCL) is a framework for jointly dealing with truth and preferences. We develop the concept of degree-based validity by lifting a Hintikka-style semantic game [10] to a provability game. Strategies in the provability game are translated into proofs in a novel labeled sequent calculus where proofs come in degrees. Furthermore, we show that preferred models can be extracted from proofs.

We introduce a cyclic proof system for the two-way alternation-free modal μ-calculus. The system manipulates one-sided Gentzen sequents and locally deals with the backwards modalities by allowing analytic applications of the cut rule. The global effect of backwards modalities on traces is handled by making the semantics relative to a specific strategy of the opponent in the evaluation game. This allows us to augment sequents by so-called trace atoms, describing traces that the proponent can construct against the opponent’s strategy. The idea for trace atoms comes from Vardi’s reduction of alternating two-way automata to deterministic one-way automata. Using the multi-focus annotations introduced earlier by Marti and Venema, we turn this trace-based system into a path-based system. We prove that our system is sound for all sequents and complete for sequents not containing trace atoms.

There are many approaches regarding the emergence of factivity in literature. Some of them who are proponents of the view that factive inferences are exported from complements, attribute it to the definiteness feature of the complements [35,28,29]. This definiteness feature can be realized covertly via a semantically-sensitive definite determiner ∆ [35], or via an overt marker (e.g., ge in Washo) [28]. Although [14] later revised their claim by calling this ge a marker of familiarity, not that of definiteness, they did not provide any evidence where the D in factive nominalized complements is not definite. This paper provides evidence from Bangla (/Bengali; an Indo-Aryan language) where an attitude verb mone pora ‘remember’ can embed nominalized complements that can be interpreted indefinitely but still remains factive. In this paper, we provide a formal compositional analysis that can account for this.

We present an axiom system for basic hybrid logic extended with propositional quantifiers (a second-order extension of basic hybrid logic) and prove its (basic and pure) strong completeness with respect to general models.

We consider the bimodal language, where the first modality is interpreted by a binary relation in the standard way, and the second is interpreted by the relation of inequality. It follows from Hughes (1990), that in this language, non-k-colorability of a graph is expressible for every finite k. We show that modal logics of classes of non-k-colorable graphs (directed or non-directed), and some of their extensions, are decidable.

A well-known problem in the theory of dependent types is how to handle so-called nested data types. These data types are difficult to program and to reason about in total dependently typed languages such as Agda and Coq. In particular, it is not easy to derive a canonical induction principle for such types. Working towards a solution to this problem, we introduce dependently typed folds for nested data types. Using the nested data type Bush as a guiding example, we show how to derive its dependently typed fold and induction principle. We also discuss the relationship between dependently typed folds and the more traditional higher-order folds.

Multi-focusing is a generalization of Andreoli’s focusing procedure which allows the parallel application of synchronous rules to multiple formulae under focus. By restricting to the class of maximally multi-focused proofs, one recovers permutative canonicity directly in the sequent calculus without the need to switch to other formalisms, e.g. proof nets, in order to represent proofs modulo permutative conversions. This characterization of canonical proofs is also amenable for the mechanization of the normalization procedure and the performance of further formal proof-theoretic investigations in interactive theorem provers. In this work we present a sequent calculus of maximally multi-focused proofs for skew non-commutative multiplicative linear logic (SkNMILL), a logic recently introduced by Uustalu, Veltri and Wan which enjoys categorical semantics in the skew monoidal closed categories of Street. The peculiarity of the multi-focused system for SkNMILL is the presence of at most two foci in synchronous phase. This reduced complexity makes it a good starting point for the formal investigations of maximally multi-focused calculi for richer substructural logics.

We show that recent approaches to static analysis based on quantitative typing systems can be extended to programming languages with global state. More precisely, we define a call-by-value language equipped with operations to access a global memory, together with a semantic model based on a (tight) multi-type system that captures exact measures of time and space related to evaluation of programs. We show that the type system is quantitatively sound and complete with respect to the operational semantics of the language.

We propose a separation logic where resources are histories (sequences) of epistemic actions so that resource update means concatenation of histories and resource decomposition means splitting of histories. This separation logic, called AMHSL, allows us to reason about the past: does what is true now depend on what was true in the past, before certain actions were executed? We show that the multiplicative connectives can be eliminated from a logical language with also epistemic and action model modalities, if the horizon of epistemic actions is bounded.

Veltman semantics is the basic Kripke-like semantics for interpretability logic. Verbrugge semantics is a generalization of Veltman semantics. An appropriate notion of bisimulation between a Verbrugge model and a Veltman model is developed in this paper. We show that a given Verbrugge model can be transformed into a bisimilar Veltman model.

We give a comprehensive account on the parameterized complexity of model checking and satisfiability of propositional inclusion and independence logic. We discover that for most parameterizations the problems are either in FPT or paraNP-complete.

Study of parallel operations such as Plotkin’s parallel-or has promoted the development of the theory of programming languages. In this paper, we consider parallel operations in the framework of categorical realizability. Given a partial combinatory algebra A equipped with an “abstract truth value” Σ (called predominance), we introduce the notions of Σ-or and Σ-and combinators in A. By choosing a suitable A and Σ, a form of parallel-or may be expressed as a Σ-or combinator. We then investigate the relationship between these combinators and the realizability model Ass(A) (the category of assemblies over A) and show the following: under a natural assumption on Σ, (i) A admits Σ-and combinator iff for any assembly X ∈ Ass(A) the Σ-subsets (canonical subassemblies) of X form a poset with respect to inclusion. (ii) A admits both Σ-and and Σ-or combinators iff for any X ∈ Ass(A) the Σ-subsets of X form a lattice with respect to intersection and union.

Subsumption-Linear Q-Resolution (SLQR) is introduced for proving theorems from Quantified Boolean Formulas. It is an adaptation of SL-Resolution, which applies to propositional and first-order logic. In turn SL-Resolution is closely related to model elimination and tableau methods. A major difference from QDPLL (DPLL adapted for QBF) is that QDPLL guesses variable assignments, while SLQR guesses clauses. In prenex QBF (PCNF, all quantifier operations are outermost) a propositional formula D is called a nontrivial consequence of a QBF Ψ if Ψ is true (has at least one model) and D is true in every model of Ψ. Due to quantifiers, one cannot simply negate D and look for a refutation, as in propositional and first-order logic. Most previous work has addressed only the case that D is the empty clause, which can never be a nontrivial consequence.

This paper shows that SLQR with the operations of resolution on both existential and universal variables as well as universal reduction is inferentially complete for closed PCNF that are free of asymmetric tautologies; i.e., if D is logically implied by Ψ, there is a SLQR derivation of D from Ψ. A weaker form called SLQR–ures omits resolution on universal variables. It is shown that SLQR–ures is not inferentially complete, but is refutationally complete for closed PCNF.