We study the exact learnability of finite unions of intersecting affine modules in one dimension. An affine module is a set of the form \(a+\sum _{j=1}^{s}b_j \mathbb {Z}\), where \(a,b_1,\ldots ,b_s\in \mathbb {N}\). We say that a set definable as a finite union of affine modules is a union of intersecting affine modules if it admits a representation in which all modules have a non-empty intersection. We show that this class is efficiently exactly learnable using equivalence and subset queries. Moreover, subset queries can be replaced with membership queries when a common element is known. Our algorithm requires at most klog (2|xℓ|) + 2k counterexamples, where k is the number of affine modules in the smallest representation and xℓ is the largest counterexample. This implies polynomial-time learnability in the binary representation.

Unification is one of the fundamental operations in automated first-order reasoning and is used intensively in fields such as theorem proving and logic programming. Since Robinson’s pioneering proposal, several efficient algorithms based on sophisticated data structures have been developed, and some approaches to its parallelization have been analyzed. Recent advances in hardware, particularly the rise of Graphical Processing Units (GPUs), give us the opportunity to work with large volumes of data in parallel. The use of GPUs is becoming increasingly common in applications beyond computer graphics, thanks to their massive parallelism, high memory bandwidth, and throughput-oriented architecture. However, these advantages are best leveraged when working with data structures that exhibit high regularity, such as dense arrays or matrices. Unfortunately, inductively defined expressions, commonly used in unification, typically exhibit irregular and sparse structures, making them unsuitable for direct GPU acceleration. In this work, we present a new approach to efficiently unify large batches of terms by introducing a novel matrix-based representation that avoids the irregularities inherent in traditional approaches. We have implemented a C-based prototype that achieves competitive performance compared to a Prolog baseline, while also revealing how structural characteristics of the representation influence efficiency. This prototype provides the foundation for a massively parallel GPU-based unification engine, which we plan to develop in future work.

In this paper, we will show how to handle a new normal form called terse normal form (TNF), which is crucial to the development of a novel tableau method that solves realizability and synthesis for specifications expressed in a safety fragment of LTL. The construction of these tableaux is based on the conversion of LTL formulas into TNF, which is one of the most computationally expensive parts of the method. We will explain how to efficiently extract the relevant information required by the tableaux without having to compute the entire TNF of a safety formula. We present a correct algorithm for carrying out this task as well as its implementation.

We present a sound and complete algorithm for the detection of independent variables in linear temporal logic formulae. These formulae are often used to specify reactive systems. The algorithm is based on the use of model checkers.

We study the realizability and strong satisfiability problems for SAFETY LTL, a syntactic fragment of Linear Temporal Logic ([Formula presented]) capturing safe formulas. While it is well-known that realizability for this fragment lies in [Formula presented], the best-known lower bound is [Formula presented]-hardness. Surprisingly, closing this gap has proven an elusive task. Previous works have claimed first [Formula presented]-completeness [1] and later [Formula presented]-completeness [2] for this problem, but both of these proofs turned out to be incorrect. We revisit the problem of the exact classification of the complexity of realizability for [Formula presented] through the lens of seemingly weaker fragments. While we cannot settle the question for [Formula presented], we study a subfragment of it consisting of formulas of the form [Formula presented], where α is a present formula over system variables and ψ contains Next as the only temporal operator. We prove that the realizability problem for this new fragment, which we call [Formula presented], is [Formula presented]-complete, and observe that this fragment is equirealizable to existing more expressive fragments, such as the class [Formula presented] [3]. Furthermore, we revisit the techniques used in the purported proof of [Formula presented]-completeness of Arteche and Hermo [1], and observe that, while incorrect in their original claims, their proofs can be modified to classify the complexity of strong satisfiability, a necessary condition for realizability introduced by Kupferman, Sadigh, and Seshia [4]. We prove that, with regards to strong satisfiability, the fragments [Formula presented] and [Formula presented] are in fact equivalent under polynomial-time many-one reductions.

When building tableau for temporal logic formulae, applying a two-pass construction, we first check the validity of the given tableaux input by creating a tableau graph, and then, in the second "pass", we check if all the eventualities are satisfied. In one-pass tableaux checking the validity of the input does not require these auxiliary constructions. This paper continues the development of one-pass tableau method for temporal logics introducing tree-style one-pass tableau systems for Computation Tree Logic (CTL) and shows how this can be extended to capture Extended CTL (ECTL). A distinctive feature here is the utilisation, for the core tableau construction, of the concept of a context of an eventuality which forces its earliest fulfilment. Relevant algorithms for obtaining a systematic tableau for these branching-time logics are also defined. We prove the soundness and completeness of the method. With these developments of a tree-shaped one-pass tableau for CTL and ECTL, we have formalisms which are well suited for the automation and are amenable for the implementation, and for the formulation of dual sequent calculi. This brings us one step closer to the application of one-pass context-based tableaux in certified model checking for a variety of CTL-type branching-time logics.

The standard model checking setup analyses whether the given system specification satisfies a dedicated temporal property of the system, providing a positive answer here or a counter-example. At the same time, it is often useful to have an explicit proof that certifies the satisfiability. This is exactly what the certified model checking (CMC) has been introduced for. The paper argues that one-pass (context-based) tableau for PLTL can be efficiently used in the CMC setting, emphasising the following two advantages of this technique. First, the use of the context in which the eventualities occur, forces them to fulfil as soon as possible. Second, a dual to the tableau sequent calculus can be used to formalise the certificates. The combination of the one-pass tableau and the dual sequent calculus enables us to provide not only counter-examples for unsatisfied properties, but also proofs for satisfied properties that can be checked in a proof assistant. In addition, the construction of the tableau is enriched by an embedded solver, to which we dedicate those (propositional) computational tasks that are costly for the tableaux rules applied solely. The combination of the above techniques is particularly helpful to reason about large (system) specifications.

Formal ontologies are axiomatizations in a logic-based formalism. The development of formal ontologies is generating considerable research on the use of automated reasoning techniques and tools that help in ontology engineering. One of the main aims is to refine and to improve axiomatizations for enabling automated reasoning tools to efficiently infer reliable information. Defects in the axiomatization cannot only cause wrong inferences, but can also hinder the inference of expected information, either by increasing the computational cost of or even preventing the inference. In this paper, we introduce a novel, fully automatic white-box testing framework for first-order logic (FOL) ontologies. Our methodology is based on the detection of inference-based redundancies in the given axiomatization. The application of the proposed testing method is fully automatic since (i) the automated generation of tests is guided only by the syntax of axioms and (ii) the evaluation of tests is performed by automated theorem provers (ATPs). Our proposal enables the detection of defects and serves to certify the grade of suitability—for reasoning purposes—of every axiom. We formally define the set of tests that are (automatically) generated from any axiom and prove that every test is logically related to redundancies in the axiom from which the test has been generated. We have implemented our method and used this implementation to automatically detect several non-trivial defects that were hidden in various FOL ontologies. Throughout the paper we provide illustrative examples of these defects, explain how they were found and how each proof—given by an ATP—provides useful hints on the nature of each defect. Additionally, by correcting all the detected defects, we have obtained an improved version of one of the tested ontologies: Adimen-SUMO.

Temporal logic has become essential for various areas in computer science, most notably for the specification and verification of hardware and software systems. For the specification purposes rich temporal languages are required that, in particular, can express fairness constraints. For linear-time logics which deal with fairness in the linear-time setting, one-pass and two-pass tableau methods have been developed. In the repository of the CTL-type branching-time setting, the well-known logics ECTL and ECTL^+ were developed to explicitly deal with fairness. However, due to the syntactical restrictions, these logics can only express restricted versions of fairness. The logic CTL^*, often considered as "the full branching-time logic" overcomes these restrictions on expressing fairness. However, this logic itself, is extremely challenging for the application of verification techniques, and the tableau technique, in particular. For example, there is no one-pass tableau construction for this logic, while it is known that one-pass tableau has an additional benefit enabling the formulation of dual sequent calculi that are often treated as more "natural" being more friendly for human understanding. Based on these two considerations, the following problem arises - are there logics that have richer expressiveness than ECTL^+ yet "simpler" than CTL^* for which a one-pass tableau can be developed? In this paper we give a solution to this problem. We present a tree-style one-pass tableau for a sub-logic of CTL^* that we call ECTL^#, which is more expressive than ECTL^+ allowing the formulation of a new range of fairness constraints with "until" operator. The presentation of the tableau construction is accompanied by an algorithm for constructing a systematic tableau, for any given input of admissible branching-time formulae. We prove the termination, soundness and completeness of the method. As tree-shaped one-pass tableaux are well suited for the automation and are amenable for the implementation and for the formulation of sequent calculi, our results also open a prospect of relevant developments of the automation and implementation of the tableau method for ECTL^#, and of a dual sequent calculi.