A Decidable Class of Nested Iterated Schemata (extended version)

Details A Decidable Class of Nested Iterated Schemata (extended version) A Decidable Class of Nested Iterated Schemata (extended version)

2010-01-24

arxiv.org/abs/1001.4251v1

Computer Science

Logic in Computer Science

43 pages, extended version of "A Decidable Class of Nested Iterated Schemata", submitted to IJCAR 2009

Scientific paper

Many problems can be specified by patterns of propositional formulae depending on a parameter, e.g. the specification of a circuit usually depends on the number of bits of its input. We define a logic whose formulae, called "iterated schemata", allow to express such patterns. Schemata extend propositional logic with indexed propositions, e.g. P_i, P_i+1, P_1, and with generalized connectives, e.g. /\i=1..n or i=1..n (called "iterations") where n is an (unbound) integer variable called a "parameter". The expressive power of iterated schemata is strictly greater than propositional logic: it is even out of the scope of first-order logic. We define a proof procedure, called DPLL*, that can prove that a schema is satisfiable for at least one value of its parameter, in the spirit of the DPLL procedure. However the converse problem, i.e. proving that a schema is unsatisfiable for every value of the parameter, is undecidable so DPLL* does not terminate in general. Still, we prove that it terminates for schemata of a syntactic subclass called "regularly nested". This is the first non trivial class for which DPLL* is proved to terminate. Furthermore the class of regularly nested schemata is the first decidable class to allow nesting of iterations, i.e. to allow schemata of the form /\i=1..n (/\j=1..n ...).

Affiliated with

Also associated with

No associations

Rating

A Decidable Class of Nested Iterated Schemata (extended version) does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with A Decidable Class of Nested Iterated Schemata (extended version), we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Decidable Class of Nested Iterated Schemata (extended version) will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-696771