This paper relates the well-known Linear Temporal Logic with the logic of propositional schemata introduced in elsewhere by the authors. We prove that LTL is equivalent to a class of schemata in the sense that polynomial-time reductions exist from one logic to the other. Some consequences about complexity are given. We report about first experiments and the consequences about possible improvements in existing implementations are analyzed.

We define a logic of propositional formula schemata adding to the syntax of propositional logic indexed propositions and iterated connectives ranging over intervals parameterized by arithmetic variables. The satisfiability problem is shown to be undecidable for this new logic, but we introduce a very general class of schemata, called bound-linear, for which this problem becomes decidable. This result is obtained by reduction to a particular class of schemata called regular, for which we provide a sound and complete terminating proof procedure. This schemata calculus allows one to capture proof patterns corresponding to a large class of problems specified in propositional logic. We also show that the satisfiability problem becomes again undecidable for slight extensions of this class, thus demonstrating that bound-linear schemata represent a good compromise between expressivity and decidability.

Looking at inference as a way of transforming information so as to make it more easily usable (or interpretable) allows to consider accepted and rejected propositions as equally relevant and naturally gives a bipolar view of reasoning. The four possibilities of transforming information from accepted or rejected propositions into accepted or rejected ones are analyzed and examples illustrating them are given. This analysis is not only interesting per se but can also be useful in increasing capabilities of existing theorem provers. A unified framework based on former work by the authors is extended by incorporating the idea of theory-anti-subsumption related to Plotkin's generalization. Working on some technical details of this framework should allow automated reasoning tools to deal with different ways of connecting accepted and rejected propositions. © 2008 Wiley Periodicals, Inc.

We define a new class of rewrite systems operating over term-graphs. Our aim is twofold. First we propose to extend classical first-order rewrite rules in order to process easily data-structures with pointers (e.g., circular lists, doubly linked lists etc). For that, our rules provide specific features such as pointer (edges) redirections, relabeling of existing nodes etc. Unfortunately, such features are very often source of non confluence. Our second aim is then to ensure confluence of the considered rewrite systems in the new class. We introduce the notion of term-graphs with priority and show that orthogonal rewrite systems are confluent in our setting

The problem of model construction is known to be a very important one. An extension of semantic tableaux (that can also be applied to the matings and to the connection method) allowing the building of models in a systematic way is presented. This approach is different from the usual one in semantic tableaux, in which model construction is a by-product of refutation failures (and this only in very particular cases). In fact, we incorporate in the object level, reasoning usually done in an ad hoc manner in the meta-level. Some of the rules introduced by this extension are essentially new. The impossibility of simulating them by the standard tableaux rules and their necessity in extending the class of captured models is shown. These rules and the modified classical ones are based on the use of equational problems. Equational problems are formulae containing only equalities and inequalities, connected by ‘and’, ‘or’ and quantified in a particular way. The method preserves the refutational completeness of semantic tableaux. It subsumes in a simpler and more powerful framework other enhancements such as the incorporation of unification. An algorithm for simultaneous search of refutations and models with extended semantic tableaux is given. One non-trivial example is treated in detail. A model is built for an example in which resolution-based procedures (i.e. resolution with ordering strategies) fails to detect satisfiability. It is also shown that in some cases our method is able to decide satisfiable formulae with only infinite models. Finally, a natural extension to some modal logics is presented.