Search

As the complexity of software systems is ever increasing, so is the need for practical tools for formal verification. Among these are automatic theorem provers, capable of solving various reasoning problems automatically, and proof assistants, capable of deriving more complex results when guided by a mathematician/programmer. In this paper we consider using the latter to build the former. In the proof assistant Isabelle/HOL we combine functional programming and logical program verification to build a theorem prover for propositional logic. We also consider how such a prover can be used to solve a reasoning task without much mental labor. The development is extended with a formalized proof system for writing machine-checked sequent calculus proofs. We consider how this can be used to teach computer science students about logic, automated reasoning and proof assistants. [ABSTRACT FROM AUTHOR]

As the complexity of software systems is ever increasing, so is the need for practical tools for formal verification. Among these are automatic theorem provers, capable of solving various reasoning problems automatically, and proof assistants, capable of deriving more complex results when guided by a mathematician/programmer. In this paper we consider using the latter to build the former. In the proof assistant Isabelle/HOL we combine functional programming and logical program verification to build a theorem prover for propositional logic. We also consider how such a prover can be used to solve a reasoning task without much mental labor. The development is extended with a formalized proof system for writing machine-checked sequent calculus proofs. We consider how this can be used to teach computer science students about logic, automated reasoning and proof assistants.

Locus computation is an essential issue in mathematics education, and a traditional feature of Dynamic Geometry software (DGS). Nowadays, the rising of new DGS programs, such as GeoGebra, merging DGS and Computer Algebra software (CAS) has fostered a combined approach to locus computation, quite performing in standard examples, but demanding an extended theoretical, and the related algorithmic counterpart, able to deal with less conventional situations. Here we formulate--and reflect about, yielding some proposals--on a few pending issues related to the protocols for the computation of parametric families of loci. Then we focus on a different source of difficulties, through the example of the very elementary and classical theorem of Thales. Thus, in the framework of the current development of automated deduction in geometry (ADG) tools, we will show how the automatic discovery of Thales's converse statement might require a locus computation that gives rise to an unexpected family of octic curves. Finally, we will exhibit how the handling (finding the equation, plotting, geometric characterization, etc.) of such curves requires the concourse of DGS and CAS programs, a mixed graphic-symbolic-numeric approach, and human-machine interaction, a cooperation that could be the basis towards achieving the required improvements concerning locus computation software. [ABSTRACT FROM AUTHOR]

Mutual exclusion algorithms are at the heart of concurrent/parallel and distributed systems. It is well known that such algorithms are very difficult to analyze, and in the literature, different conjectures about starvation freedom and the number of by-passes (also called the overtaking factor) exist. The overtaking factor affects the (hopefully) bounded waiting time that a process competing for entering the critical section has to suffer before accessing the shared resource. This paper proposes a novel modeling approach based on Timed Automata and the Uppaal toolset, which proves effective for studying all the properties of a mutual exclusion algorithm for N ≥ 2 processes, by exhaustive model checking. Although the approach, as already confirmed by similar experiments reported in the literature, is not scalable due to state explosion problems and can be practically applied until N ≤ 5 , it is of great value for revealing the true properties of analyzed algorithms. For dimensions N > 5 , the Statistical Model Checker of Uppaal can be used, which, although based on simulations, can confirm properties by estimations and probabilities. This paper describes the proposed modeling and verification method and applies it to several mutual exclusion algorithms, thus retrieving known properties but also showing new results about properties often studied by informal reasoning. [ABSTRACT FROM AUTHOR]

We apply automated reasoning to investigation of finite factors of algebraic structures associated with knot diagrams. We refute "double size" conjecture about cancellative semigroups and keis. [ABSTRACT FROM AUTHOR]

This is a report on the project "Axiomatizing Conditional Normative Reasoning" (ANCoR, M 3240-N) funded by the Austrian Science Fund (FWF). The project aims to deepen our understanding of conditional normative reasoning by providing an axiomatic study of it at the propositional but also first-order level. The focus is on a particular framework, the so-called preference-based logic for conditional obligation, whose main strength has to do with the treatment of contrary-to-duty reasoning and reasoning about exceptions. The project considers not only the meta-theory of this family of logics but also its mechanization. [ABSTRACT FROM AUTHOR]

Mutual exclusion algorithms are at the heart of concurrent/parallel and distributed systems. It is well known that such algorithms are very difficult to analyze, and in the literature, different conjectures about starvation freedom and the number of by-passes (also called the overtaking factor) exist. The overtaking factor affects the (hopefully) bounded waiting time that a process competing for entering the critical section has to suffer before accessing the shared resource. This paper proposes a novel modeling approach based on Timed Automata and the Uppaal toolset, which proves effective for studying all the properties of a mutual exclusion algorithm for N≥2 processes, by exhaustive model checking. Although the approach, as already confirmed by similar experiments reported in the literature, is not scalable due to state explosion problems and can be practically applied until N≤5, it is of great value for revealing the true properties of analyzed algorithms. For dimensions N>5, the Statistical Model Checker of Uppaal can be used, which, although based on simulations, can confirm properties by estimations and probabilities. This paper describes the proposed modeling and verification method and applies it to several mutual exclusion algorithms, thus retrieving known properties but also showing new results about properties often studied by informal reasoning.

In ontology engineering, reusing (or extending) ontologies poses a significant challenge, requiring revising their ontological commitments and ensuring accurate representation and coherent reasoning. This study aims to address two main objectives. Firstly, it seeks to develop a methodological approach supporting ontology extension practices. Secondly, it aims to demonstrate its feasibility by applying the approach to the case of extending qualitative spatial reasoning (QSR) theories. Key questions involve effectively interpreting spatial extensions while maintaining consistency. The framework systematically analyzes extensions of formal ontologies, providing a reconstruction of a qualitative calculus. Reconstructed qualitative calculus demonstrates improved interpretative capabilities and reasoning accuracy. The research underscores the importance of methodological approaches when extending formal ontologies, with spatial interpretation serving as a valuable case study.

In ontology engineering, reusing (or extending) ontologies poses a significant challenge, requiring revising their ontological commitments and ensuring accurate representation and coherent reasoning. This study aims to address two main objectives. Firstly, it seeks to develop a methodological approach supporting ontology extension practices. Secondly, it aims to demonstrate its feasibility by applying the approach to the case of extending qualitative spatial reasoning (QSR) theories. Key questions involve effectively interpreting spatial extensions while maintaining consistency. The framework systematically analyzes extensions of formal ontologies, providing a reconstruction of a qualitative calculus. Reconstructed qualitative calculus demonstrates improved interpretative capabilities and reasoning accuracy. The research underscores the importance of methodological approaches when extending formal ontologies, with spatial interpretation serving as a valuable case study. [ABSTRACT FROM AUTHOR]

Artificially intelligent systems are nowadays presented as systems that should, among other things, be explainable and ethical. In parallel, both in the popular culture and within the scientific literature, there is a tendency to anthropomorphize Artificial Intelligence (AI) and reify intelligent systems as persons. From the perspective of machine ethics and ethical AI, this has resulted in the belief that truly autonomous ethical agents (i.e., machines and algorithms) can be defined, and that machines could, by themselves, behave ethically and perform actions that are justified (explainable) from a normative (ethical) standpoint. Under this assumption, and given that utilities and risks are generally seen as quantifiable, many scholars have seen consequentialism (or utilitarianism) and rational choice theory as likely candidates to be implemented in automated ethical decision procedures, for instance to assess and manage risks as well as maximize expected utility. While some see this implementation as unproblematic, there are important limitations to such attempts that need to be made explicit so that we can properly understand what artificial autonomous ethical agents are, and what they are not. From the perspective of explainable AI, there are value-laden technical choices made during the implementation of automated ethical decision procedures that cannot be explained as decisions made by the system. Building on a recent example from the machine ethics literature, we use computer simulations to study whether autonomous ethical agents can be considered as explainable AI systems. Using these simulations, we argue that technical issues with ethical ramifications leave room for reasonable disagreement even when algorithms are based on ethical and rational foundations such as consequentialism and rational choice theory. By doing so, our aim is to illustrate the limitations of automated behavior and ethical AI and, incidentally, to raise awareness on the limits of so-called autonomous ethical agents. [ABSTRACT FROM AUTHOR]

Formalisms based on temporal logics interpreted over finite strict linear orders, known in the literature as finite traces, have been used for temporal specification in automated planning, process modelling, (runtime) verification and synthesis of programs, as well as in knowledge representation and reasoning. In this article, we focus on first-order temporal logic on finite traces. We first investigate preservation of equivalences and satisfiability of formulas between finite and infinite traces, by providing a set of semantic and syntactic conditions to guarantee when the distinction between reasoning in the two cases can be blurred. Moreover, we show that the satisfiability problem on finite traces for several decidable fragments of first-order temporal logic is ExpSpace-complete, as in the infinite trace case, while it decreases to NExpTime when finite traces bounded in the number of instants are considered. This leads also to new complexity results for temporal description logics over finite traces. Finally, we investigate applications to planning and verification, in particular by establishing connections with the notions of insensitivity to infiniteness and safety from the literature. [ABSTRACT FROM AUTHOR]

We propose an automated procedure to prove polyhedral abstractions (also known as polyhedral reductions) for Petri nets. Polyhedral abstraction is a new type of state space equivalence, between Petri nets, based on the use of linear integer constraints between the marking of places. In addition to defining an automated proof method, this paper aims to better characterize polyhedral reductions, and to give an overview of their application to reachability problems. Our approach relies on encoding the equivalence problem into a set of SMT formulas whose satisfaction implies that the equivalence holds. The difficulty, in this context, arises from the fact that we need to handle infinite-state systems. For completeness, we exploit a connection with a class of Petri nets, called flat nets, that have Presburger-definable reachability sets. We have implemented our procedure, and we illustrate its use on several examples. [ABSTRACT FROM AUTHOR]

We describe the foundations and the systematization of natural logic-like monotonic inference using unscoped episodic logical forms (ULFs) that as reported by Kim et al. (Proceedings of the 1st and 2nd Workshops on Natural Logic Meets Machine Learning (NALOMA), Groningen, 2021a, b) introduced and first evaluated. In addition to providing a more detailed explanation of the theory and system, we present results from extending the inference manager to address a few of the limitations that as reported by Kim et al. (Proceedings of the 1st and 2nd Workshops on Natural Logic Meets Machine Learning (NALOMA), Groningen, 2021b) naive system has. Namely, we add mechanisms to incorporate lexical information from the hypothesis (or goal) sentence, enable the inference manager to consider multiple possible scopings for a single sentence, and match against the goal using English rather than the ULF. [ABSTRACT FROM AUTHOR]

We present an approach for representing abstract argumentation frameworks based on an encoding into classical higher-order logic. This provides a uniform framework for computer-assisted assessment of abstract argumentation frameworks using interactive and automated reasoning tools. This enables the formal analysis and verification of meta-theoretical properties as well as the flexible generation of extensions and labellings with respect to well-known argumentation semantics. [ABSTRACT FROM AUTHOR]

We use a quite simple, yet challenging, elementary geometry statement, the so-called "never proved" (by a mathematician) theorem, introduced by Prof. Jiawei Hong in his communication to the IEEE 1986 Symposium on Foundations of Computer Science, to exemplify and analyze the current situation of achievements, ongoing improvements and limitations of GeoGebra's automated reasoning tools, as well as other computer algebra systems, in dealing with geometric inequalities. We present a large collection of facts describing the curious (and confusing) history behind the statement and its connection to automated deduction. An easy proof of the "never proved" theorem, relying on some previous (but not trivial) human work is included. Moreover, as part of our strategy to address this challenging result with automated tools, we formulate a large list of variants of the "never proved" statement (generalizations, special cases, etc.). Addressing such variants with GeoGebra Discovery, ${\texttt{Maple}}$, ${\texttt{REDUCE/Redlog}}$ or ${\texttt{Mathematica}}$ leads us to introduce and reflect on some new approaches (e.g., partial elimination of quantifiers, consideration of symmetries, relevance of discovery vs. proving, etc.) that could be relevant to consider for future improvements of automated reasoning in geometry algorithms. As a byproduct, we obtain an original result (to our knowledge) concerning the family of triangles inscribable in a given triangle.

The interest in quantum computing has grown rapidly in recent years, and with it grows the importance of securing quantum circuits. A novel type of threat to quantum circuits that dedicated attackers could launch are power trace attacks. To address this threat, this paper presents first formalization and demonstration of using power traces to unlock and steal quantum circuit secrets. With access to power traces, attackers can recover information about the control pulses sent to quantum computers. From the control pulses, the gate level description of the circuits, and eventually the secret algorithms can be reverse engineered. This work demonstrates how and what information could be recovered. This work uses algebraic reconstruction from power traces to realize two new types of single trace attacks: per-channel and total power attacks. The former attack relies on per-channel measurements to perform a brute-force attack to reconstruct the quantum circuits. The latter attack performs a single-trace attack using Mixed-Integer Linear Programming optimization. Through the use of algebraic reconstruction, this work demonstrates that quantum circuit secrets can be stolen with high accuracy. Evaluation on 32 real benchmark quantum circuits shows that our technique is highly effective at reconstructing quantum circuits. The findings not only show the veracity of the potential attacks, but also the need to develop new means to protect quantum circuits from power trace attacks. Throughout this work real control pulse information from real quantum computers is used to demonstrate potential attacks based on simulation of collection of power traces.

First-order logic automated theorem proving is an important research content in the fields of knowledge representation and automated reasoning. How to effectively select clauses to participate in deduction is a research hotspot to improve the capability and efficiency of automated reasoning. Based on the good de-duction characteristics of multi-clause dynamic deduction, this paper proposes a measure and calculation method of clause activity and complexity by analyzing the properties of the variable terms and the structure of function terms of clauses, which can effectively evaluate clauses with different term structures. Based on the clause evaluation method, a multi-clause dynamic deduction algorithm with fully synergized deduction of clauses is proposed, which can effectively optimize the multi-clause deduction search path. The multi-clause dynamic deduction algorithm is applied to the international top prover Eprover 2.6, and the 2021 international automated reasoning competition problems (FOF group) is used as the test object. Within the standard 300 seconds, Eprover 2.6 with the proposed multi-clause dynamic deduction algorithm proven four more theorems than the original Eprover 2.6, and the average proof time is decreases by 1.12 seconds under the condition of proving the same number of theorems as Eprover 2.6. In addition, it can prove 16 unproven theorems of Eprover 2.6, accounting for 15.1% of the total unproven theorems. The experimental results show that the proposed multi-clause dynamic deduction algorithm is an effective inference method, which can improve the capability and time efficiency of automated reasoning to a certain extent. [ABSTRACT FROM AUTHOR]

In this note, I present my personal view on the interaction of the three areas Automated Programming, Symbolic Computation, and Machine Learning. Programming is the activity of finding a (hopefully) correct program (algorithm) for a given problem. Programming is central to automation in all areas and is considered one of the most creative human activities. However, already very early in the history of programming, people started to "jump to the meta-level" of programming, i.e., started to develop procedures that automate, or semi-automate, (various aspects or parts of) the process of programming. This area has various names like "Automated Programming", "Automated Algorithm Synthesis", etc. Developing compilers can be considered an early example of a problem in automated programming. Automated reasoners for proving the correctness of programs with respect to a specification is an advanced example of a topic in automated programming. ChatGPT producing (amazingly good) programs from problem specifications in natural language is a recent example of automated programming. Programming tends to become the most important activity as the level of technological sophistication increases. Therefore, automating programming is maybe the most exciting and relevant technological endeavor today. It also will have enormous impact on the global job market in the software industry. Roughly, I see two main approaches to automated programming: symbolic computation and machine learning. In this note, I explain how the two approaches work and that they are fundamentally different because they address two completely different ways of how problems are specified. Together, the two approaches constitute (part of) what some people like to call "artificial intelligence". In my analysis, both approaches are just part of (algorithmic) mathematics. The approaches, like all non-trivial mathematical methods, need quite some intelligence on the side of the human inventors of the methods. However, applying the methods is just "machine execution" of algorithms. It is misleading to call the application "machine intelligence" or "artificial intelligence". The analysis of the two approaches to automated programming also suggests that the two approaches, in the future, should be combined to achieve even higher levels of sophistication. At the end of this note, I propose some research questions for this new direction. [ABSTRACT FROM AUTHOR]

Cyclic induction is a powerful reasoning technique that consists in blocking the proof development of certain subgoals already encountered during the proof process. In the setting of first-order logic with inductive definitions and equality (FOLID), cyclic proofs can be built automatically by the Cyclist prover, but their implementations are error-prone and the human validation may be tedious. On the other hand, cyclic induction is not yet integrated into certifying proof environments that support first-order logic and inductive definitions, such as Isabelle and Coq. We propose a solution to check, using Coq, the cyclic proofs produced by E-Cyclist, an extension of Cyclist that implements a more efficient soundness validation method, by using the general Noetherian induction principle integrated into Coq. Our work is based on a methodology for certifying first-order formula-based Noetherian induction proofs, such as those based on implicit induction. The advantages of our approach are threefold: - I) The certification of cyclic FOLID proofs is mechanical. Coq can validate every single step from the E-Cyclist proofs, as well as the induction arguments; also, it helps to identify errors in a very precise way. - II) There is a great potential for automation. The methodology has already been used to automatically convert to Coq scripts implicit induction proofs. - III) Cyclic induction can be directly performed in Coq. Coq functions are provided to manage the induction part. [ABSTRACT FROM AUTHOR]

We use a quite simple, yet challenging, elementary geometry statement, the so-called "never proved" (by a mathematician) theorem, introduced by Prof. Jiawei Hong in his communication to the IEEE 1986 Symposium on Foundations of Computer Science, to exemplify and analyze the current situation of achievements, ongoing improvements and limitations of GeoGebra's automated reasoning tools, as well as other computer algebra systems, in dealing with geometric inequalities. We present a large collection of facts describing the curious (and confusing) history behind the statement and its connection to automated deduction. An easy proof of the "never proved" theorem, relying on some previous (but not trivial) human work is included. Moreover, as part of our strategy to address this challenging result with automated tools, we formulate a large list of variants of the "never proved" statement (generalizations, special cases, etc.). Addressing such variants with GeoGebra Discovery, Maple, REDUCE/Redlog or Mathematica leads us to introduce and reflect on some new approaches (e.g., partial elimination of quantifiers, consideration of symmetries, relevance of discovery vs. proving, etc.) that could be relevant to consider for future improvements of automated reasoning in geometry algorithms. As a byproduct, we obtain an original result (to our knowledge) concerning the family of triangles inscribable in a given triangle. [ABSTRACT FROM AUTHOR]

Simulation games are designed to cultivate expertise and rehearse particular skill sets. To yield longitudinal effects, sequences of events must be crafted to yield intended learning outcomes, sometimes by focusing on particularly difficult situations and replaying variants. The present paper develops a logic-based approach for encoding the interrelation between action, events, and objects in a manner that allows the resulting scenario description to immediately be executed in a game development environment. This has the dual effect of decoupling the description of a scenario from the simulation platform itself, as well as supporting iterative and flexible development of learning content. To this end, we provide three interrelated components: First, we develop a scenario description language based on Answer Set Programming. The language is designed to allow an automated reasoner to deduce a schedule of the future events that are caused by an action taken in a given simulation environment. Second, we define a protocol for exchanging actions and computed futures between, respectively, the simulation environment and the external automated reasoner. Finally, as a proof of concept, we develop an Application Programming Interface (API) for the Unity Real-Time Development Platform that implements the protocol and offers a software framework for connecting the computed future events to concrete game objects. This allows the game to evolve coherently from the specification. We argue that the resulting system inherits capabilities for artificial commonsense reasoning from its declarative basis which are useful for reasoning about an evolving emergency incident or training scenario. [ABSTRACT FROM AUTHOR]

There is an increasing number of cyber-systems (e.g., systems for payment, transportation, voting, critical infrastructures) whose security depends intrinsically on human users. In this paper, we introduce a novel approach for the formal and automated analysis of security ceremonies. A security ceremony expands a security protocol to include human nodes alongside computer nodes, with communication links that comprise user interfaces, human-to-human communication and transfers of physical objects that carry data, and thus a ceremony's security analysis should include, in particular, the mistakes that human users might make when participating actively in the ceremony. Our approach defines mutation rules that model possible behaviors of a human user, automatically generates mutations in the behavior of the other agents of the ceremony to match the human-induced mutations, and automatically propagates these mutations through the whole ceremony. This allows for the analysis of the original ceremony specification and its possible mutations, which may include the way in which the ceremony has actually been implemented or could be implemented. To automate our approach, we have developed the tool X-Men, which is a prototype that builds on top of Tamarin, one of the most common tools for the automatic unbounded verification of security protocols. As a proof of concept, we have applied our approach to three real-life case studies, uncovering a number of concrete vulnerabilities. Some of these vulnerabilities were so far unknown, whereas others had so far been discovered only by empirical observation of the actual ceremony execution or by directly formalizing alternative models of the ceremony by hand, but X-Men instead allowed us to find them automatically. [ABSTRACT FROM AUTHOR]