The DLS algorithm
Elimination of all predicates.
Enter second-order formula:
Generate all solutions and choose the shortest (default = no)
Generate the output unformated (default = no)
Example of a filled in form
Main page
|
Circumscription page
|
NAT page
|
Syntax