Pozvánka na seminář
Přednáška - : Decidable Fragments of First Order Modal Logic
@Seminář aplikované matematické logiky13.12.2023 16:00
First Order Modal Logic (FOML) extends First Order Logic (FO) with modal operators. FOML is suitable for many applications including planning, predicate epistemic logics among others. However, FOML is computationally unfriendly. Most of the decidable fragments of FO that are decidable (like the two variable fragment, guarded fragment, restriction to unary predicates) become undecidable when extended with modal operators. Until recently, the only known decidable fragment of FOML was the monodic fragment. In this talk we will discuss some new and interesting decidable fragments of FOML and its variants that we have identified. This talk includes some of the results from the speaker's PhD thesis (supervised by R. Ramanujam) and some results in collaboration with Mo Liu, R. Ramanujam and Yanijing Wang.
Přednáška - : A Tour of Substructural Interpolation
@Seminář aplikované matematické logiky08.11.2023 16:00
"Interpolation" refers to a cluster of fundamental metalogical properties with applications spanning hardware and software verification, databases, and many other areas. In this talk, we survey the state of the art on interpolation in substructural logics, focusing in particular on big-picture features that shed some light on the nature of interpolation generally. We will also discuss some of the most important remaining open questions and on-going efforts to solve them.
Přednáška - : Maximum satisfiability problem in the real-valued MV-algebra
@Seminář aplikované matematické logiky01.11.2023 16:00
In propositional Boolean logic, maximum satisfiability (MaxSAT) problem can be viewed as a generalization of the SAT problem. An input to the SAT problem is a CNF formula (a list of clauses) and the question is whether there is an assignment that satisfies all of them. MaxSAT is an optimization problem, namely to determine the maximum number of satisfied clauses in the list, over all assignments. Our work addresses the MaxSAT problem problem for a list of arbitrary formulas in the language of propositional Łukasiewicz logic, over the semantics provided by the MV-algebra on the real interval [0,1]. First we reduce the MaxSAT problem to the SAT problem in the same semantics. This provides a classification against which other approaches to the problem can be compared. Then we define a tableau-like method that eventually yields one or more systems of linear constraints, similar to the earlier approaches of Hähnle or Olivetti. This is joint work with Felip Manya and Amanda Vidal, presented at Tableaux 2023.
Přednáška - : Negated Implications in Connexive Relevant Logics
@Seminář aplikované matematické logiky04.10.2023 16:00
Adding connexive theses to relevant logics has the unsavoury result of allowing one to prove every negated implication. In this talk, I'll diagnose this problem, and consider some avenues by which this result can be avoided.
Přednáška - : Fuzzy Information States and Fuzzy Support
@Seminář aplikované matematické logiky07.06.2023 16:00
The semantic framework for representing questions known as inquisitive semantics is based on a relation of support relating formulas and information states (modeled as sets of possible worlds). In my talk I will discuss two ways of fuzzifying inquisitive semantics. The first one replaces crisp information states with fuzzy information states (modeled as fuzzy sets of possible worlds). The second one replaces the crisp notion of support with a notion of fuzzy support. I will show some properties of the resulting framework. For example, I will show that if we fuzzify inquisitive semantics in these two different directions, we obtain an abstract and very general version of a principle known from the basic inquisitive semantics as Truth-Support Bridge. I will also sketch some open questions related to this approach.
Přednáška - : Everyone Knows that Everyone Knows
@Seminář aplikované matematické logiky17.05.2023 16:00
A gossip protocol is a procedure for sharing secrets in a network. The basic action in a gossip protocol is a telephone call wherein the calling agents exchange all the secrets they know. An agent who knows all secrets is an expert. The usual termination condition, given a finite number of agents, is that all agents are experts. We report on research investigating the termination condition that all agents know that all agents are experts. If agents only exchange secrets, there is no knowledge of the time, and no knowledge of the protocol, even stronger termination conditions are unreachable. Furthermore, n-2 + (n choose 2) calls are optimal to reach this epistemic goal. Although it is easy to come up with schedules achieving this, it is remarkably non-trivial to show that they are optimal.
Přednáška - : A Simplified Lower Bound on Intuitionistic Implicational Proofs
@Seminář aplikované matematické logiky10.05.2023 16:00
One of the major open problems in classical proof complexity is to prove super-polynomial lower bounds on the length of proofs in Frege (aka Hilbert-style) systems, or equivalently, sequent calculus or natural deduction. Interestingly, exponential lower bounds are known for some non-classical logics (modal, superintuitionistic, substructural), starting with seminal work of Hrubeš (2007); they are all based on variants of the feasible disjunction property that play a similar role as monotone feasible interpolation for classical proof systems. This might suggest that the presence of disjunction is essential for these lower bounds, but Jeřábek (2017) adapted them to the purely implicational fragment of intuitionistic logic. This results in a complex argument employing an implicational translation of intuitionistic logic on top of the proof of the lower bound proper, which in turn relies on monotone circuit lower bounds (Razborov, Alon–Boppana). In this talk, I will show how to prove the exponential lower bound directly for intuitionistic implicational logic without any translations, using a simple argument based on an efficient version of Kleene’s slash. Apart from Frege, it applies directly to sequent calculus and (dag-like) natural deduction, obviating also the need for translation of these proof systems to Frege. One motivation for this work comes from presistent claims by Gordeev and Haeusler, who purport to show that all intuitionistic implicational tautologies have polynomial-size dag-like natural deduction proofs, implying NP = PSPACE. Their claims are false as they contradict the above-mentioned exponential lower bounds (and, in fact, also older exponential lower bounds on constant-depth proofs), but for a non-specialist, understanding this requires tracking down multiple papers and some reading between the lines. Our argument consolidates all proof-theoretic components of the lower bound into one simple proof, depending only on the Alon–Boppana circuit lower bound.
Přednáška - : How to compute uniform interpolant semantically
@Seminář aplikované matematické logiky03.05.2023 16:00
This talk will be a tutorial of a known technique on computing uniform interpolants by examining finite (or finitely generated) algebras and their extensions. We will focus on intermediate logics, but the method is reasonably general.
Přednáška - : Promise Model Checking Problems over a Fixed Model
@Seminář aplikované matematické logiky19.04.2023 16:00
The fixed-template constraint satisfaction problem (CSP) can be seen as the problem of deciding whether a given primitive positive first-order sentence is true in a fixed structure (also called model). We study a class of problems that generalizes the CSP simultaneously in two directions: we fix a set L of quantifiers and Boolean connectives, and we specify two versions of each constraint, one strong and one weak. Given a sentence which only uses symbols from L, the task is to distinguish whether the sentence is true in the strong sense, or it is false even in the weak sense. We classify the computational complexity of these problems for the existential positive equality-free fragment of first-order logic and we prove some upper and lower bounds for the positive equality-free fragment. The partial results are sufficient, e.g., for all extensions of the latter fragment. This is a joint work with Kristina Asimi and Silvia Butti.
Přednáška - : Computational Content of a Generalized Kreisel-Putnam Rule
@Seminář aplikované matematické logiky22.03.2023 16:00
In this talk, we propose a computational interpretation of the generalized Kreisel-Putnam rule, also known as the generalized Harrop rule or simply the Split rule, in the style of BHK semantics. We will achieve this by exploiting the Curry-Howard correspondence between formulas and types. First, we inspect the inferential behavior of the Split rule in the setting of a natural deduction system for the intuitionistic propositional logic. This will guide our process of formulating an appropriate program that would capture the corresponding computational content of the typed Split rule. In other words, we want to find an appropriate selector function for the Split rule by considering its typed variant. Our investigation can also be reframed as an effort to answer the following questions: is the Split rule constructively valid? Our answer is positive for the Split rule as well as for its newly proposed generalized versions.
Přednáška - : First-Order Proof Schemata and Inductive Proof Analysis
@Seminář aplikované matematické logiky08.03.2023 16:00
Proofs are more than just validations of theorems; they can contain interesting mathematical information like bounds or algorithms. However this information is frequently hidden and proof transformations are required to make it explicit. One such transformation on proofs in sequent calculus is cut-elimination (i.e. the removal of lemmas in formal proofs to obtain proofs made essentially of the syntactic material of the theorem). In his famous paper ``Untersuchungen ueber das logische Schliessen'' Gentzen showed that for cut-free proofs of prenex end-sequents Herbrand's theorem can be realized via the midsequent theorem. In fact Gentzen defined a transformation which, given a cut-free proof p of a prenex sequent S, constructs a cut-free proof p' of a sequent S' (a so-called Herbrand sequent) which is propositionally valid and is obtained by instantiating the quantifiers in S. These instantiations may contain interesting and compact information on the validity of S. Generally, the construction of Herbrand sequents requires cut-elimination in a given proof p (or at least the elimination of quantified cuts). The method CERES (cut-elimination by resolution) provides an algorithmic tool to compute a Herbrand sequent S' from a proof p (with cuts) of S even without constructing a cut-free version of p. A prominent and crucial principle in mathematical proofs is mathematical induction. However, in proofs with mathematical induction Herbrand's theorem typically fails. To overcome this problem we replace induction by recursive definitions and proofs by proof schemata. An extension of CERES to proof schemata (CERESs) allows to compute inductive definitions of Herbrand expansions (so-called Herbrand systems) representing infinite sequences of Herbrand sequents, resulting in a form of Herbrand's theorem for inductive proofs.
Přednáška - : One-variable RQ & RS5: A Frame Based Equivalence
@Seminář aplikované matematické logiky01.03.2023 16:00
Often, for a propositional logic L, some one-variable fragment of L's first order extension corresponds to some modal logic on L. For the relevant logic R, it seems that the one-variable fragment of RQ (the stronger of R's two standard first-order extensions) corresponds to the modal relevant logic RS5 (the S5ish axiomatic extension of R which contains classical S5 in translation). This talk is a work in progress showing this equivalence. One direction of the equivalence is obtained by transforming first-order models into modal models. The other direction is (almost) obtained by evaluating all of RQ in a particular modal model. I also discuss some philosophical upshots/consequences of this result.
Přednáška - : Kleene Algebra With Tests for Weighted Programs
@Seminář aplikované matematické logiky25.01.2023 16:00
Weighted programs generalize probabilistic programs and offer a framework for specifying and encoding mathematical models by means of an algorithmic representation. Kleene algebra with tests is an algebraic formalism based on regular expressions with applications in proving program equivalence. We extend the language of Kleene algebra with tests so that it is sufficient to formalize reasoning about a simplified version weighted programs. We introduce relational semantics for the extended language, and we generalize the relational semantics to an appropriate extension of Kleene algebra with tests, called Kleene algebra with weights and tests. We demonstrate by means of an example that Kleene algebra with weights and tests offers a simple algebraic framework for reasoning about equivalence and optimal runs of weighted programs.
Přednáška - : A Parametrised Axiomatization for a Large Number of Restricted Second-Order Logics
@Seminář aplikované matematické logiky11.01.2023 16:00
By limiting the range of the predicate variables in a second-order language one may obtain restricted versions of second-order logic such as weak second-order logic or definable subset logic. In this note we provide an infinitary strongly complete axiomatization for several systems of this kind having the range of the predicate variables as a parameter. The completeness argument uses simple techniques from the theory of Boolean algebras.