Name
Abstract | ||
|---|---|---|
Two distinct algorithms are presented to extract (schemata of) resolution proofs from closed tableaux for propositional schemata [4]. The first one handles the most efficient version of the tableau calculus but generates very complex derivations (denoted by rather elaborate rewrite systems). The second one has the advantage that much simpler systems can be obtained, however the considered proof procedure is less efficient. In [2, 4] a tableau calculus (called Stab) is presented for reasoning on schemata of propositional problems. This proof procedure is able to test the validity of logical formulae built on a set of indexed propositional symbols, using generalized connectives such as W n=1 or V n=1 , where i,n are part of the language (n denotes a parameter, i.e. an existentially quantified variable). A schema is unsatisfiable iff it is unsatisfiable for every value of n. Stab combines the usual expansion rules of propositional logic with some delayed instantiation schemes that perform a case-analysis on the value of the parameter n. Termination is ensured for a specific class of schemata, called regular, thanks to a loop detection rule which is able to prune infinite tableaux into finite ones, by encoding a form a mathematical induction (by “descente infinie”). A related algorithm, called Dpll ∗ and based on an extension of the Davis-Putnam-Logemann-Loveland procedure, is presented in [3]. In the present work, we show that resolution proofs can be automatically extracted from the closed tableaux constructed by Stab or Dpll ∗ on unsatisfiable schemata. More precisely, we present an algorithm that, given a closed tableau T for a schema φn, returns a schema of a refutation of φn in the resolution calculus [9]. In the usual propositional case, it is well-known that algorithms exist to extract resolution proofs from closed tableaux constructed either by the usual structural rules [11, 13] or by the DPLL algorithm [7, 6]. The resolution proofs are used in various applications, for instance for certification [14], for abstraction-refinement [10] or for explanations generation [8]. The present paper extends these techniques to propositional schemata. Beside the previously mentioned applications, this turned out to be particularly important in the context of the ASAP project [1] in which schemata calculi are applied to the formalisation and analysis of mathematical proofs via cut-elimination. Indeed, the algorithm used for cut-elimination, called CERES [5], explicitly relies |
Year | Venue | Keywords |
|---|---|---|
2011 | CoRR | artificial intelligent |
Field | DocType | Volume |
Discrete mathematics,Algebra,Computer science,Mathematical proof,Artificial intelligence,Proof procedure,Schema (psychology),Machine learning | Journal | abs/1106.2692 |
Citations | PageRank | References |
0 | 0.34 | 9 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vincent Aravantinos | 1 | 86 | 10.29 |
| Nicolas Peltier | 2 | 50 | 11.84 |