A resolution calculus for first-order schemata (Q2843818)

The paper under review proposes a new resolution calculus which is appropriate for analysing the satisfiability of schemata of propositional clause sets. Other decision procedures regarding the satisfiability problem for the subclasses of regular, regularly nested and bound-linear propositional schemata have been provided by \textit{V. Aravantinos} et al. [Lect. Notes Comput. Sci. 5607, 32--46 (2009; Zbl 1260.03011); ibid. 6173, 293--308 (2010; Zbl 1291.03014); J. Artif. Intell. Res. (JAIR) 40, 599--656 (2011; Zbl 1220.68087)], respectively. However, the decision procedure presented in this paper is applicable to a logic whose expressive power is strictly greater than that of the languages considered in the mentioned works.NEWLINENEWLINEThe syntax and semantics considered in this paper are very similar to those of a simple subclass of clausal logic. The only particularity is the consideration of a special set of constant symbols, called parameters, that denote natural numbers and must be interpreted as elements of \(\mathbb{N}\).NEWLINENEWLINEFirstly, a resolution calculus is presented and proven to be sound (w.r.t. the mentioned semantics). Nevertheless, only a very weak form of completeness is established for that calculus.NEWLINENEWLINEThen, a slightly simpler language is proposed which, roughly speaking, is formed only by so-called normalized clause sets (which, in particular, contain at most one parameter). It is shown that no loss of expressiveness is entailed by the additional syntactic restrictions imposed. More precisely, it is exposed how schemata of propositional formulas that are outside the class of normalized clause sets (as, for example, schemata with several parameters) can be encoded into normalized clause sets. It is noted that this class of schemata is similar, but more general, than the class of regular schemata and it is not comparable to the classes of regularly nested and bound-linear schemata.NEWLINENEWLINEAfterwards, relying on the simpler language proposed, the calculus is extended by a loop detection rule (that is based on so-called levels of sets of clauses and) which is able to ensure both completeness and termination (provided the rules are applied in a fair way). Roughly speaking, the pruning rule that is added to the calculus is able to detect the existence of a cycle in a derivation and, when that is the case, it generates a clause of the form \(n < k\) (where \(n\) is the parameter and \(k\) is a natural number) -- called a pruning clause -- which can be safely added (in the sense of retaining satisfiability) into the clause set under consideration at that step of the derivation. Furthermore, the inclusion of the generated pruning clause in the clause set automatically bounds the value of the parameter and the problem becomes essentially equivalent to a propositional one. It is shown that this extended calculus is sound, refutationally complete and terminating. Moreover, it is remarked that it follows from the termination proof presented that, regarding its time complexity, the algorithm is at most doubly exponential.NEWLINENEWLINEThe last endeavour provided in the paper consists of the extension of the proposed calculus to first-order clauses. This extension is straightforward (it is done, as usual, by lifting). However, the resulting calculus is neither terminating nor even refutationally complete (since the satisfiability problem is not semi-decidable for schemata of first-order clause sets).