Efficient checking of term ordering constraints

Alexandre Riazanov; Andrei Voronkov

Efficient checking of term ordering constraints

Alexandre Riazanov, Andrei Voronkov

Research output: Chapter in Book/Conference proceeding › Conference contribution

Abstract

Simplification orderings on terms play a crucial role in reducing the search space in paramodulation-based theorem proving. Such a use of orderings requires checking simple ordering constraints on substitutions as an essential part of many operations. Due to their frequency, such checks are costly and are a good target for optimisation. In this paper we present an efficient implementation technique for checking constraints in one of the most widely used simplification orderings, the Knuth-Bendix ordering. The technique is based on the idea of runtime algorithm specialisation, which is a close relative of partial evaluation.

Original language	English
Title of host publication	Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)\|Lect Notes Artif Intell
Editors	D. Basin
Publisher	Springer Nature
Pages	60-74
Number of pages	14
Volume	3097
Publication status	Published - 2004
Event	Second International Joint Conference, IJCAR 2004 - Cork Duration: 1 Jul 2004 → … http://dblp.uni-trier.de/db/conf/cade/ijcar2004.html#RiazanovV04http://dblp.uni-trier.de/rec/bibtex/conf/cade/RiazanovV04.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/cade/RiazanovV04

Publication series

Name	Lecture Notes in Computer Science

Conference

Conference	Second International Joint Conference, IJCAR 2004
City	Cork
Period	1/07/04 → …
Internet address	http://dblp.uni-trier.de/db/conf/cade/ijcar2004.html#RiazanovV04http://dblp.uni-trier.de/rec/bibtex/conf/cade/RiazanovV04.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/cade/RiazanovV04

Access to Document

Cite this

@inproceedings{0e4bc7a072b2414fbeb023b40d40eb2c,

title = "Efficient checking of term ordering constraints",

abstract = "Simplification orderings on terms play a crucial role in reducing the search space in paramodulation-based theorem proving. Such a use of orderings requires checking simple ordering constraints on substitutions as an essential part of many operations. Due to their frequency, such checks are costly and are a good target for optimisation. In this paper we present an efficient implementation technique for checking constraints in one of the most widely used simplification orderings, the Knuth-Bendix ordering. The technique is based on the idea of runtime algorithm specialisation, which is a close relative of partial evaluation.",

author = "Alexandre Riazanov and Andrei Voronkov",

year = "2004",

language = "English",

volume = "3097",

series = "Lecture Notes in Computer Science",

publisher = "Springer Nature",

pages = "60--74",

editor = "D. Basin",

booktitle = "Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)|Lect Notes Artif Intell",

address = "United States",

note = "Second International Joint Conference, IJCAR 2004 ; Conference date: 01-07-2004",

url = "http://dblp.uni-trier.de/db/conf/cade/ijcar2004.html\#RiazanovV04http://dblp.uni-trier.de/rec/bibtex/conf/cade/RiazanovV04.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/cade/RiazanovV04",

}

Riazanov, A & Voronkov, A 2004, Efficient checking of term ordering constraints. in D Basin (ed.), Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)|Lect Notes Artif Intell. vol. 3097, Lecture Notes in Computer Science, Springer Nature, pp. 60-74, Second International Joint Conference, IJCAR 2004, Cork, 1/07/04. <http://dblp.uni-trier.de/db/conf/cade/ijcar2004.html#RiazanovV04>

Efficient checking of term ordering constraints. / Riazanov, Alexandre; Voronkov, Andrei.
Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)|Lect Notes Artif Intell. ed. / D. Basin. Vol. 3097 Springer Nature, 2004. p. 60-74 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Conference proceeding › Conference contribution

TY - GEN

T1 - Efficient checking of term ordering constraints

AU - Riazanov, Alexandre

AU - Voronkov, Andrei

PY - 2004

Y1 - 2004

N2 - Simplification orderings on terms play a crucial role in reducing the search space in paramodulation-based theorem proving. Such a use of orderings requires checking simple ordering constraints on substitutions as an essential part of many operations. Due to their frequency, such checks are costly and are a good target for optimisation. In this paper we present an efficient implementation technique for checking constraints in one of the most widely used simplification orderings, the Knuth-Bendix ordering. The technique is based on the idea of runtime algorithm specialisation, which is a close relative of partial evaluation.

AB - Simplification orderings on terms play a crucial role in reducing the search space in paramodulation-based theorem proving. Such a use of orderings requires checking simple ordering constraints on substitutions as an essential part of many operations. Due to their frequency, such checks are costly and are a good target for optimisation. In this paper we present an efficient implementation technique for checking constraints in one of the most widely used simplification orderings, the Knuth-Bendix ordering. The technique is based on the idea of runtime algorithm specialisation, which is a close relative of partial evaluation.

UR - https://www.scopus.com/pages/publications/9444291407

M3 - Conference contribution

VL - 3097

T3 - Lecture Notes in Computer Science

SP - 60

EP - 74

BT - Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science)|Lect Notes Artif Intell

A2 - Basin, D.

PB - Springer Nature

T2 - Second International Joint Conference, IJCAR 2004

Y2 - 1 July 2004

ER -

Efficient checking of term ordering constraints

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this