PigeonHolePrinciple

gapt.examples.PigeonHolePrinciple

Constructs a formula representing the pigeon hole principle. More precisely: PigeonHolePrinciple( p, h ) states that if p pigeons are put into h holes then there is a hole which contains two pigeons. PigeonHolePrinciple( p, h ) is a tautology iff p > h.

Since we want to avoid empty disjunctions, we assume > 1 pigeons.

Attributes

Graph
Supertypes
class Object
trait Matchable
class Any
Self type

Members list

Value members

Concrete methods

def apply(ps: Int, hs: Int): FOLFormula

Value parameters

hs

the number of holes

ps

the number of pigeons

Attributes

def hole(i: Int): FOLConst
def inHole(p: Int, h: Int): FOLAtom
def pigeon(i: Int): FOLConst

Concrete fields

val rel: String

The binary relation symbol.

The binary relation symbol.

Attributes