Skip to main content

Research Repository

Advanced Search

Outputs (20)

Planar tautologies hard for resolution (2001)
Presentation / Conference Contribution
Dantchev, S., & Riis, S. (2001, October). Planar tautologies hard for resolution. Presented at 42nd IEEE Symposium of Foundations of Computer Science, Las Vegas, Nev

We prove exponential lower bounds on the resolution proofs of some tautologies, based on rectangular grid graphs. More specifically, we show a 2/sup /spl Omega/(n)/ lower bound for any resolution proof of the mutilated chessboard problem on a 2n/spl... Read More about Planar tautologies hard for resolution.

An implementation of LF with coercive subtyping & universes (2001)
Journal Article
Callaghan, P., & Luo, Z. (2001). An implementation of LF with coercive subtyping & universes. Journal of Automated Reasoning, 27(1), 3-27. https://doi.org/10.1023/a%3A1010648911114

We present Plastic, an implementation of LF with Coercive Subtyping, and focus on its implementation of Universes. LF is a variant of Martin-Löf''s logical framework, with explicitly typed -abstractions. We outline the system of LF with its extension... Read More about An implementation of LF with coercive subtyping & universes.

Tree resolution proofs of the weak pigeon-hole principle (2001)
Presentation / Conference Contribution
Dantchev, S., & Riis, S. (2001, June). Tree resolution proofs of the weak pigeon-hole principle. Presented at 16th Annual IEEE Conference on Computational Complexity, Chicago, Ill

We prove that any optimal tree resolution proof of PHPn m is of size 2&thetas;(n log n), independently from m, even if it is infinity. So far, only a 2Ω(n) lower bound has been known in the general case. We also show that any, not necessarily optimal... Read More about Tree resolution proofs of the weak pigeon-hole principle.

Wavefront correction using a self-referencing phase conjugation system based on a Zernike cell (2001)
Journal Article
Dale, S., Love, G., Myers, R., & Naumov, A. (2001). Wavefront correction using a self-referencing phase conjugation system based on a Zernike cell. Optics Communications, 191(1-2), 31-38. https://doi.org/10.1016/s0030-4018%2801%2901116-6

A wavefront correction system was produced using a phase conjugating method based on a point diffraction interferometer, or Zernike cell. This has the main advantage that no separate reference beam is required. The PDI was constructed using an optica... Read More about Wavefront correction using a self-referencing phase conjugation system based on a Zernike cell.

Two extensions of the Shapley value for cooperative games (2001)
Journal Article
Driessen, T., & Paulusma, D. (2001). Two extensions of the Shapley value for cooperative games. Mathematical Methods of Operations Research, 53(1), 35-49. https://doi.org/10.1007/s001860000099

Two extensions of the Shapley value are given. First we consider a probabilistic framework in which certain consistent allocation rules such as the Shapley value are characterized. The second generalization of the Shapley value is an extension to the... Read More about Two extensions of the Shapley value for cooperative games.

The new FIFA rules are hard: complexity aspects of sports competitions (2001)
Journal Article
Kern, W., & Paulusma, D. (2001). The new FIFA rules are hard: complexity aspects of sports competitions. Discrete Applied Mathematics, 108(3), 317-323. https://doi.org/10.1016/s0166-218x%2800%2900241-9

Consider a soccer competition among various teams playing against each other in pairs (matches) according to a previously determined schedule. At some stage of the competition one may ask whether a particular team still has a (theoretical) chance to... Read More about The new FIFA rules are hard: complexity aspects of sports competitions.

A generic greedy algorithm, partially-ordered graphs and NP-completeness (2001)
Presentation / Conference Contribution
Puricella, A., & Stewart, I. (2001, June). A generic greedy algorithm, partially-ordered graphs and NP-completeness. Presented at 27th International Workshop on Graph-Theoretic Concepts in Computer Science (WG 2001), Rostock, Germany

Let π be any fixed polynomial-time testable, non-trivial, hereditary property of graphs. Suppose that the vertices of a graph G are not necessarily linearly ordered but partially ordered, where we think of this partial order as a collection of (possi... Read More about A generic greedy algorithm, partially-ordered graphs and NP-completeness.

On a hierarchy involving transitive closure logic and existential second-order quantification (2001)
Journal Article
Gault, R., & Stewart, I. (2001). On a hierarchy involving transitive closure logic and existential second-order quantification. Logic Journal of the IGPL, 9(6), 769-780. https://doi.org/10.1093/jigpal/9.6.769

We study a hierarchy of logics where each formula of each logic in the hierarchy consists of a formula of a certain fragment of transitive closure logic prefixed with an existentially quantified tuple of unary relation symbols. By playing an Ehrenfeu... Read More about On a hierarchy involving transitive closure logic and existential second-order quantification.

The complexity of maximal constraint languages (2001)
Presentation / Conference Contribution
Bulatov, A., Krokhin, A., & Jeavons, P. (2001, December). The complexity of maximal constraint languages. Presented at 33rd ACM Symposium on the Theory of Computing(STOC), Crete, Greece

Many combinatorial search problems can be expressed as “constraint satisfaction problems” using an appropriate “constraint language”, that is, a set of relations over some fixed finite set of values. It is well-known that there is a trade-off between... Read More about The complexity of maximal constraint languages.