Related papers: Polarized Rewriting and Tableaux in B Set Theory

We present a type system for strategy languages that express program transformations as compositions of rewrite rules. Our row-polymorphic type system assists compiler engineers to write correct strategies by statically rejecting non…

We explore the Collatz conjecture and its variants through the lens of termination of string rewriting. We construct a rewriting system that simulates the iterated application of the Collatz function on strings corresponding to mixed…

Alloy is formal modeling language based on first-order relational logic, with no specific support for specifying reactive systems. We propose the usage of temporal logic to specify such systems, and show how bounded model checking can be…

The neural rings and ideals as an algebraic tool for analyzing the intrinsic structure of neural codes were introduced by C.~Curto et al. in 2013. Since then they were investigated in several papers, including the 2017 paper by…

Let $G$ be a finite group. Then there exists a first-order statement $S(G)$ in the language of rings without parameters and depending only on $G$ such that, for any field $K$, we have that $K\models S(G)$ if and only if $K$ has a Galois…

Table foundation models bring high hopes to data science: pre-trained on tabular data to embark knowledge or priors, they should facilitate downstream tasks on tables. One specific challenge is that of data semantics: numerical entries take…

We define a fragment of monadic infinitary second-order logic corresponding to an abstract separation property. We use this to define the concept of a separation subclass. We use model theoretic techniques and games to show that separation…

This paper presents a rewriting-logic-based modeling and analysis technique for physical systems, with focus on thermal systems. The contributions of this paper can be summarized as follows: (i) providing a framework for modeling and…

A number of machine learning models have been proposed with the goal of achieving systematic generalization: the ability to reason about new situations by combining aspects of previous experiences. These models leverage compositional…

In this paper, we explore the concept of modularity in first-order answer set programming (ASP). We introduce a new formalism called parametric modular logic programs, which allows defining subprograms with parameters and intensionality…

Model checking and automated theorem proving are two pillars of formal methods. This paper investigates model checking from an automated theorem proving perspective, aiming at combining the expressiveness of automated theorem proving and…

This talk describes how a combination of symbolic computation techniques with first-order theorem proving can be used for solving some challenges of automating program analysis, in particular for generating and proving properties about the…

We introduce an operational rewriting-based semantics for strictly positive nested higher-order (co)inductive types. The semantics takes into account the "limits" of infinite reduction sequences. This may be seen as a refinement and…

In recent years, G\"odel's ontological proof and variations of it were formalized and analyzed with automated tools in various ways. We supplement these analyses with a modeling in an automated environment based on first-order logic…

Several authors devised type-based termination criteria for ML-like languages allowing non-structural recursive calls. We extend these works to general rewriting and dependent types, hence providing a powerful termination criterion for the…

We establish a natural translation from word rewriting systems to strictly positive polymodal logics. Thereby, the latter can be considered as a generalization of the former. As a corollary we obtain examples of undecidable strictly…

We consider the problem of computing optimal generalised policies for relational Markov decision processes. We describe an approach combining some of the benefits of purely inductive techniques with those of symbolic dynamic programming…

The Stratified Foundations are a restriction of naive set theory where the comprehension scheme is restricted to stratifiable propositions. It is known that this theory is consistent and that proofs strongly normalize in this theory.…

In this article, we develop a positive characteristic analogue of the Bernstein--Sato theory for holonomic D-modules in the complex setting. We work with D-modules on a Noetherian regular $F$-finite $\mathbb{F}_p$-scheme $X$, and define…

This talk is devoted mainly to the concept of higher-order polarization on a group, which is introduced in the framework of a Group Approach to Quantization, as a powerful tool to guarantee the irreducibility of quantizations and/or…