We study two fundamental questions in neuro-symbolic computing: can deep learning tackle challenging problems in logics end-to-end, and can neural networks learn the semantics of logics. In this work we focus on linear-time temporal logic (LTL), as it is widely used in verification. We train a Transformer on the problem to directly predict a solution, i.e. a trace, to a given LTL formula. The training data is generated with classical solvers, which, however, only provide one of many possible solutions to each formula. We demonstrate that it is sufficient to train on those particular solutions to formulas, and that Transformers can predict solutions even to formulas from benchmarks from the literature on which the classical solver timed out. Transformers also generalize to the semantics of the logics: while they often deviate from the solutions found by the classical solvers, they still predict correct solutions to most formulas.
University of Corunna（拉科鲁尼亚大学）；University of Potsdam（波茨坦大学）
We present an overview on Temporal Logic Programming under the perspective of its application for Knowledge Representation and declarative problem solving. Such programs are the result of combining usual rules with temporal modal operators, as in Linear-time Temporal Logic (LTL). We focus on recent results of the non-monotonic formalism called Temporal Equilibrium Logic (TEL) that is defined for the full syntax of LTL, but performs a model selection criterion based on Equilibrium Logic, a well known logical characterization of Answer Set Programming (ASP). We obtain a proper extension of the s…
Léonard de Vinci Pôle Universitaire, Research Center（列奥纳多·达·芬奇大学中心研究中心）；Conservatoire National des Arts et Métiers（法国国立工艺学院）
We aim at improving reasoning on inconsistent and uncertain data. We focus on knowledge-graph data, extended with time intervals to specify their validity, as regularly found in historical sciences. We propose principles on semantics for efficient Maximum A-Posteriori inference on the new Temporal Markov Logic Networks (TMLN) which extend the Markov Logic Networks (MLN) by uncertain temporal facts and rules. We examine total and partial temporal (in)consistency relations between sets of temporal formulae. Then we propose a new Temporal Parametric Semantics, which may combine several sub-functi…
We describe a natural deduction formalization of intuitionistic and classical propositional logic in the Isabelle/Pure framework. In contrast to earlier work, where we explored the pedagogical benefits of using a deep embedding approach to logical modelling, here we employ a logical framework modelling. This gives rise to simple and natural teaching examples and we report on the role it played in teaching our Automated Reasoning course in 2020 and 2021.
Proof assistants are important tools for teaching logic. We support this claim by discussing three formalizations in Isabelle/HOL used in a recent course on automated reasoning. The first is a formalization of System W (a system of classical propositional logic with only two primitive symbols), the second is the Natural Deduction Assistant (NaDeA), and the third is a one-sided sequent calculus that uses our Sequent Calculus Verifier (SeCaV). We describe each formalization in turn, concentrating on how we used them in our teaching, and commenting on features that are interesting or useful from …
We present a novel approach for teaching logic and the metatheory of logic to students who have some experience with functional programming. We define concepts in logic as a series of functional programs in the language of the proof assistant Isabelle/HOL. This allows us to make notions which are often unclear in textbooks precise, to experiment with definitions by executing them, and to prove metatheoretical theorems in full detail. We have surveyed student perceptions of our teaching approach to determine its usefulness and found that students felt that our formalizations helped them underst…
Teaching logic effectively requires an understanding of the factors which cause logic students to struggle. Formalization exercises, which require the student to produce a formula corresponding to the natural language sentence, are a good candidate for scrutiny since they tap into the students' understanding of various aspects of logic. We correlate the difficulty of formalization exercises predicted by a previously proposed difficulty estimation algorithm with two empirical difficulty measures on the Grade Grinder corpus, which contains student solutions to FOL exercises. We obtain a moderate…
The Logical Expressiveness of Temporal GNNs via Two-Dimensional Product Logics
RPTU Kaiserslautern-Landau（亚琛工业大学凯撒斯劳滕-兰道分校）；Queen Mary University of London（伦敦女王大学）；University of Łódź（卢宾大学）；Theoretical Computer Science / Formal Methods（理论计算机科学/形式方法）；University of Kassel（卡塞尔大学）
University of Trieste（的里雅斯特大学）；Saarland University（萨尔大学）；University of Technology, Vienna（维也纳技术大学）
We discuss how to define a kernel for Signal Temporal Logic (STL) formulae. Such a kernel allows us to embed the space of formulae into a Hilbert space, and opens up the use of kernel-based machine learning algorithms in the context of STL. We show an application of this idea to a regression problem in formula space for probabilistic models.
University of Oxford（牛津大学）；Monash University（莫纳什大学）
In this paper, we study the problem of learning to satisfy temporal logic specifications with a group of agents in an unknown environment, which may exhibit probabilistic behaviour. From a learning perspective these specifications provide a rich formal language with which to capture tasks or objectives, while from a logic and automated verification perspective the introduction of learning capabilities allows for practical applications in large, stochastic, unknown environments. The existing work in this area is, however, limited. Of the frameworks that consider full linear temporal logic or ha…
The heterogeneity of tools that support temporal logic formulae poses several challenges in terms of interoperability. In particular, a standard syntax for temporal logic on finite traces, despite similar to the one for infinite traces, is currently missing. This document proposes a standard grammar for several temporal logic formalisms interpreted over finite traces, like Linear Temporal Logic (LTLf), Linear Dynamic Logic (LDLf), Pure-Past Linear Temporal Logic (PLTLf) and Pure-Past Linear Dynamic Logic (PLDLf).
We use the algebraic framework for languages of infinite trees introduced in [4] to derive effective characterisations of various temporal logics, in particular the logic EF (a fragment of CTL) and its counting variant cEF.
In this paper, we consider a temporal logic planning problem in which the objective is to find an infinite trajectory that satisfies an optimal selection from a set of soft specifications expressed in linear temporal logic (LTL) while nevertheless satisfying a hard specification expressed in LTL. Our previous work considered a similar problem in which linear dynamic logic for finite traces (LDLf), rather than LTL, was used to express the soft constraints. In that work, LDLf was used to impose constraints on finite prefixes of the infinite trajectory. By using LTL, one is able not only to impos…
本报告介绍了开发和使用的在线教学工具，让学生练习逻辑建模，或\emph{formalisation}，因为它是所谓的旧文献。该网站的最初版本“Logic for Fun”可追溯到2001年，但除了澳大利亚国立大学的一小群学生外，很少有人使用。目前正在用一个新的版本取代它，该版本对所有因特网用户免费，打算作为在线和传统逻辑课程的有益补充加以广泛推广。
We consider Gödel temporal logic ($\sf GTL$), a variant of linear temporal logic based on Gödel--Dummett propositional logic. In recent work, we have shown this logic to enjoy natural semantics both as a fuzzy logic and as a superintuitionistic logic. Using semantical methods, the logic was shown to be {\sc pspace}-complete. In this paper we provide a deductive calculus for $\sf GTL$, and show this calculus to be sound and complete for the above-mentioned semantics.
Temporal logics over finite traces are not the same as temporal logics over potentially infinite traces. Roşu first proved completeness for linear temporal logic on finite traces (LTLf) with a novel coinductive axiom. We offer a different proof, with fewer, more conventional axioms. Our proof is a direct adaptation of Kröger and Merz's Henkin-Hasenjaeger-style proof. The essence of our adaption is that we "inject" finiteness: that is, we alter the proof structure to ensure that models are finite. We aim to present a thorough, accessible proof.
