MPI-INF/SWS Research Reports 1991-2021

2. Number - only D1


An implementation of the Hopcroft and Tarjan planarity test and embedding algorithm

Mehlhorn, Kurt

October 1993, 20 pages.

Status: available - back from printing

We design new inference systems for total orderings by applying rewrite techniques to chaining calculi. Equality relations may either be specified axiomatically or built into the deductive calculus via paramodulation or superposition. We demonstrate that our inference systems are compatible with a concept of (global) redundancy for clauses and inferences that covers such widely used simplification techniques as tautology deletion, subsumption, and demodulation. A key to the practicality of chaining techniques is the extent to which so-called variable chainings can be restricted. Syntactic ordering restrictions on terms and the rewrite techniques which account for their completeness considerably restrict variable chaining. We show that variable elimination is an admissible simplification techniques within our redundancy framework, and that consequently for dense total orderings without endpoints no variable chaining is needed at all.

  • Attachement: (187 KBytes); MPI-I-93-151.pdf (373 KBytes)

URL to this document:

Hide details for BibTeXBibTeX
  AUTHOR = {Mehlhorn, Kurt},
  TITLE = {An implementation of the Hopcroft and Tarjan planarity test and embedding algorithm},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-93-151},
  MONTH = {October},
  YEAR = {1993},
  ISSN = {0946-011X},