Name
Abstract | ||
|---|---|---|
We devise a resolution calculus that tests the satisfiability of infinite families of clause sets, called clause set schemata. For schemata of propositional clause sets, we prove that this calculus is sound, refutationally complete, and terminating. The calculus is extended to first-order clauses, for which termination is lost, since the satisfiability problem is not semi-decidable for nonpropositional schemata. The expressive power of the considered logic is strictly greater than the one considered in our previous work. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.3233/FI-2013-855 | Fundam. Inform. |
Keywords | Field | DocType |
first-order schemata,satisfiability problem,clause set schema,infinite family,considered logic,resolution calculus,propositional clause set,clause set,expressive power,previous work,nonpropositional schema,first order logic,schemata,propositional logic | Discrete mathematics,Situation calculus,Boolean satisfiability problem,Satisfiability,Zeroth-order logic,Propositional calculus,First-order logic,Normalization property,Schema (psychology),Mathematics,Calculus | Journal |
Volume | Issue | ISSN |
125 | 2 | 0169-2968 |
Citations | PageRank | References |
7 | 0.56 | 12 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vincent Aravantinos | 1 | 86 | 10.29 |
| Mnacho Echenim | 2 | 95 | 15.75 |
| Nicolas Peltier | 3 | 50 | 11.84 |