Homomorphism Counts:  Expressive Power and Query Algorithms

A classical result by Lovász asserts that two graphs G and H are isomorphic if and only if they have the same left profile, that is, for every graph F, the number of homomorphisms from F to G coincides with the number of homomorphisms from F to H. A similar result is also known to hold for right profiles, that is, two graphs G and H are isomorphic if and only if for every graph F, the number of homomorphisms from G to F coincides with the number of homomorphisms from H to F. During the past several years, there has been a study of equivalence relations that are relaxations of isomorphism obtained by restricting the left profile or the right profile to suitably restricted classes of graphs, instead of the class of all graphs. Furthermore, a notion of a query algorithm based on homomorphism counts was recently introduced and investigated. The aim of this talk is to present an overview of some of the main results in this area with emphasis on the connections with finite model theory and constraint satisfaction.

Strong completeness of a first-order temporal logic for real time

Propositional temporal logic over the real number time flow is finitely axiomatisable, but its first-order counterpart is not recursively axiomatisable. We study the logic that combines the propositional axiomatisation with the usual axioms for first-order logic with identity, and develop an alternative “admissible” semantics for it, showing that it is strongly complete for admissible models over the reals. By contrast there is no recursive axiomatisation of the first-order temporal logic of admissible models whose time flow is the integers, or any scattered linear ordering.

What is a formal proof?

This talk investigates the question: what is a formal logical proof (in general -- as opposed to: what is a formal proof in this or that specific proof system)?  I begin by setting out a core conception of formal proof and then spend the remainder of the talk considering whether we should add to it the requirement that proofs be feasibly (polynomial time) checkable.  One argument in favour of this addition is that in its absence, the core conception allows each formula of propositional logic to count as its own proof (i.e. a proof of its own unsatisfiability, or satisfiability, or validity, as the case may be). I undermine this argument by showing that adding the requirement of feasible proof-checking does not avoid a proliferation of self-proving formulas.  I also counter two other arguments for the feasibility condition.  The conclusion is that we do not have good reason to add such a condition to the core conception of formal proof presented at the beginning of the talk.

Partial and False Information

In algebraic terms, partiality and inconsistency are duals of one another, but in informational semantics, they have a closer connection with one another. I include misinformation and disinformation as information. Misinformation may arise from facts and an underlying reliable (although not perfectly reliable) network enabling information flow. We are often confronted with incorrect information that arises from the fact that we do not have access to certain salient facts about the network or about the origin of the information. Taking this sort of circumstance into account requires a non-monotonic view of the relationship between the information available in limited situations and that contained by the universe as a whole. A formal semantical account of this relationship is explained in this talk.

Logics for Reasoning about Strategic Abilities of Socially Interacting Rational Agents

An important aspect of socially interacting rational agents are the strategic abilities of individual agents and groups (coalitions) of agents to guarantee the achievement of their desired goals, while acting and interacting within an entire society of agents. Several logical systems have been proposed for formalising and capturing such reasoning were introduced the early 2000s, starting with the Coalition Logic (CL), the Alternating Time Temporal Logic (ATL), and some extensions of these. 

Coalition Logic provides a natural, but rather restricted perspective: the agents in the proponent coalition are viewed as acting in full cooperation with each other but in complete opposition to all agents outside of the coalition, which are thus treated as adversaries. The Alternating Time Temporal Logic extends Coalition Logic with temporal operators allowing for expressing long-term temporised goals. 

The strategic interaction in real societies is much more complex, usually involving various patterns combining cooperation and competition. To capture these, more expressive and versatile logical frameworks are needed. 

In this talk I will give a brief overview of some of these, and will then focus on the Logic of Coalitional Goal Assignments  (LCGA), capturing reasoning about strategic abilities of the entire society to cooperate in order to ensure achievement of the societal goals, while simultaneously protecting the abilities of individuals and groups within the society to achieve their individual and group goals. 

The talk will be based mainly on the following references: 

1. V. Goranko: Logics for Strategic Reasoning of Socially Interacting Rational Agents: An Overview and Perspectives, Logics, vol. 1(1), 2023. 

Available from: https://www.mdpi.com/2813-0405/1/1/3. 

2. S. Enqvist and V. Goranko: The temporal logic of coalitional goal assignments in concurrent multi-player games, ACM Transactions of Computational Logic, Vol. 23, No. 4, Article 21, 2022. Available from https://arxiv.org/abs/2012.14195.  

Further key references: 

1.     M. Pauly: A Modal Logic for Coalitional Power in Games, Journal of Logic and Computation, Vol. 12(1), 2002, pp. 149166.

Available from https://academic.oup.com/logcom/article-pdf/12/1/149/3657514/120149.pdf.

2.     R. Alur, T.A. Henzinger, and O. Kupferman: Alternating-time temporal logic. Journal of the ACM 49:672-713, 2002. 

(only pages 1-19). Available from https://www.cis.upenn.edu/~alur/Jacm02.pdf 

3.     W. van der Hoek and M.J.W. Wooldridge: Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications, Studia Logica,75:1, pp. 125 { 157, 2003. Available from https://link.springer.com/content/pdf/10.1023/A:1026185103185.pdf

4.     V. Goranko and S. Enqvist: Socially Friendly and Group Protecting Coalition Logics, Proc. of AAMAS'2018, IFAAMAS publ., 2018, pp 372{380. Available from http://ifaamas.org/Proceedings/aamas2018/pdfs/p372.pdf.

5.     V. Goranko and F. Ju: A Logic for Conditional Local Strategic Reasoning, Journal of Logic, Language and Information, 2021, special issue of LORI VII, vol. 31, pp167{188, 2022. Available from https://arxiv.org/abs/2102.06148.pdf.