A C F I N O S T V W X

A

and(Formula, Formula) - Static method in class cnf.CNF

Erzeugt die Konjunktion zweier Formeln.

and(List<Formula>) - Static method in class cnf.CNF

Erzeugt die Konjunktion einer Liste von Formeln.

and(Formula...) - Static method in class cnf.CNF

Erzeugt die Konjunktion einer Liste von Formeln.

C

cnf - package cnf

CNF - Class in cnf

Methoden zur Konstruktion von aussagenlogischen Formeln sowie zum Aufruf eines SAT-Solvers.

F

ff() - Static method in class cnf.CNF

Erzeugt die immer falsche Formel.

Formula - Class in cnf

Repraesentation aussagenlogischer Formeln.

I

iff(Formula, Formula) - Static method in class cnf.CNF

Erzeugt die Biimplikation zweier Formeln.

imp(Formula, Formula) - Static method in class cnf.CNF

Erzeugt die Implikation zweier Formeln.

N

neg(Formula) - Static method in class cnf.CNF

Erzeugt die Negation einer gegbenen Formel.

O

or(Formula, Formula) - Static method in class cnf.CNF

Erzeugt die Disjunktion zweier Formeln.

or(List<Formula>) - Static method in class cnf.CNF

Erzeugt die Disjunktion einer Liste von Formeln.

or(Formula...) - Static method in class cnf.CNF

Erzeugt die Disjunktion einer Liste von Formeln.

S

satisfiable(Formula) - Static method in class cnf.CNF

Wandelt die uebergebene Formel in eine erfuellbarkeitsaequivalente Formel in CNF um und ueberprueft sie mittels des SAT-Solvers SAT4j auf Erfuellbarkeit.

T

toString() - Method in class cnf.Formula

Wandelt die repraesentierte Formel in einen String um.

tt() - Static method in class cnf.CNF

Erzeugt die immer wahre Formel.

V

var(Object) - Static method in class cnf.CNF

Erzeugt die Formel, die durch eine aussagenlogische Variable gegeben ist.

W

writeDIMACS(OutputStream, Formula) - Static method in class cnf.CNF

Wendet die Tseitin-Transformation an und schreibt das Ergebnis im DIMACS-Format in den os.

X

xor(Formula, Formula) - Static method in class cnf.CNF

Erzeugt das exklusive Oder zweier Formeln.

A C F I N O S T V W X