相关论文: A Rewriting Logic Approach to Specification, Proof…

We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof…

Properties expressed as the provability of a first-order sentence can be disproved by just finding a model of the negation of the sentence. This fact, however, is meaningful in restricted cases only, depending on the shape of the sentence…

Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving…

We consider the problem of automated reasoning about dynamically manipulated data structures. The state-of-the-art methods are limited to the unfold-and-match (U+M) paradigm, where predicates are transformed via (un)folding operations…

We propose a procedure for automated implicit inductive theorem proving for equational specifications made of rewrite rules with conditions and constraints. The constraints are interpreted over constructor terms (representing data values),…

Structural proof theory is praised for being a symbolic approach to reasoning and proofs, in which one can define schemas for reasoning steps and manipulate proofs as a mathematical structure. For this to be possible, proof systems must be…

Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles…

We introduce a sound and complete coinductive proof system for reachability properties in transition systems generated by logically constrained term rewriting rules over an order-sorted signature modulo builtins. A key feature of the…

In this paper we study the logical foundations of automated inductive theorem proving. To that aim we first develop a theoretical model that is centered around the difficulty of finding induction axioms which are sufficient for proving a…

In this paper we develop cyclic proof systems for the problem of inclusion between the least sets of models of mutually recursive predicates, when the ground constraints in the inductive definitions belong to the quantifier-free fragments…

Combining a standard proof search method, such as resolution or tableaux, and rewriting is a powerful way to cut off search space in automated theorem proving, but proving the completeness of such combined methods may be challenging. It may…

Automated theorem proving has long been a key task of artificial intelligence. Proofs form the bedrock of rigorous scientific inquiry. Many tools for both partially and fully automating their derivations have been developed over the last…

An inductive theorem proving method for constrained term rewriting systems, which is based on rewriting induction, needs a decision procedure for reduction-completeness of constrained terms. In addition, the sufficient complete property of…

We design a proof system for propositional classical logic that integrates two languages for Boolean functions: standard conjunction-disjunction-negation and binary decision trees. We give two reasons to do so. The first is…

Cyber-physical systems are inherently complex due to their connection between software and the physical world. Iterative design reduces their complexity, but increases the need to repeatedly recheck their safety in full after every change.…

Reachability Logic is a formalism that can be used, among others, for expressing partial-correctness properties of transition systems. In this paper we present three proof systems for this formalism, all of which are sound and complete and…

Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus involving induction and co-induction. These proof principles…

Many semantical aspects of programming languages, such as their operational semantics and their type assignment calculi, are specified by describing appropriate proof systems. Recent research has identified two proof-theoretic features that…

This study empirically validates automated logical specification methods for behavioural models, focusing on their robustness, scalability, and reproducibility. By the systematic reproduction and extension of prior results, we confirm key…

We propose a new cyclic proof system for automated, equational reasoning about the behaviour of pure functional programs. The key to the system is the way in which cyclic proof and equational reasoning are mediated by the use of contextual…