cl-banner

Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion

Haruhiko Sato and Sarah Winkler

Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Lecture Notes in Artificial Intelligence 9195, pp. 152 – 162, 2015.

Abstract

This paper describes two advancements of SAT-based Knuth-Bendix completion as implemented in Maxcomp. (1) Termination techniques using the dependency pair framework are encoded as satisfiability problems, including dependency graph and reduction pair processors. (2) Instead of relying on pure maximal completion, different SAT-encoded control strategies are exploited.
Experiments show that these developments let Maxcomp improve over other automatic completion tools, and produce novel complete systems.

 

  PDF |    doi:10.1007/978-3-319-21401-6_10  |  © Springer International Publishing Switzerland

BibTeX 

@inproceedings{HSSW-CADE15,
author = "Haruhiko Sato and Sarah Winkler",
title = "Encoding Dependency Pair Techniques and Control Strategies
for Maximal Completion",
booktitle = "Proceedings of the 25th International Conference on Automated Deduction (CADE-25)",
editor = "Amy Felty and Aart Middeldorp",
series = "Lecture Notes in Artificial Intelligence",
volume = 9195,
pages = "152--162",
year = 2015,
doi = "10.1007/978-3-319-21401-6_10"
}
Nach oben scrollen