Wyniki wyszukiwania - BazTech

Ograniczanie wyników

1 Fundamenta Informaticae

1 2007

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Sortuj według:

Ogranicz wyniki do:

A Propositional Proof System with Quantification Over Permutations

Herman G., Paterson T., Soltys M.

Fundamenta Informaticae

2007

Vol. 79, nr 1-2

71-83

We introduce a new propositional proof system, which we call H, that allows quantification over permutations. In H we may write ($ab)a and ("ab)a, which is semantically equivalent to a(a,b)Úa(b,a) and a(a,b)U`a(b,a), respectively. We show that H with cuts restricted to S1 formulas (we denote this system H1) simulates efficiently the Hajós calculus (HC) for constructing graphs which are non-3-colorable. This shows that short proofs over formulas that assert the existence of permutations can capture polynomial time reasoning (as by [9], HC is equivalent in strength to EF, which in turn captures polytime reasoning). We also show that EF simulates efficiently H1*, which is H1 with proofs restricted to being tree-like. In short, we show that [formula]