English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

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

MPS-Authors
/persons/resource/persons45021

Mehlhorn,  Kurt
Algorithms and Complexity, MPI for Informatics, Max Planck Society;

/persons/resource/persons45092

Mutzel,  Petra
Algorithms and Complexity, MPI for Informatics, Max Planck Society;

/persons/resource/persons45100

Näher,  Stefan
Algorithms and Complexity, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

MPI-I-93-151.pdf
(Any fulltext), 373KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Mehlhorn, K., Mutzel, P., & Näher, S.(1993). An implementation of the Hopcroft and Tarjan planarity test and embedding algorithm (MPI-I-93-151). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-B42B-8
Abstract
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.