Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Journal of Automated Reasoning

11-02-2019

Using Well-Founded Relations for Proving Operational Termination

Author: Salvador Lucas

Published in: Journal of Automated Reasoning

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

In this paper, we study operational termination, a proof theoretical notion for capturing the termination behavior of computational systems. We prove that operational termination can be characterized at different levels by means of well-founded relations on specific formulas which can be obtained from the considered system. We show how to obtain such well-founded relations from logical models which can be automatically generated using existing tools.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now
Appendix
Available only for authorised users
Footnotes
2
The labels of the rules refer to such a system: \( SR \) stands for subject reduction, \( M1 \) and \( M2 \) for membership-1/-2, \( Rf \) for reflexivity, \( Rl \) for replacement, and \( T \) for transitivity.
 
3
Some new labels referring to such a system are used now: \( M1 \) for membership-1 and \( C \) for congruence.
 
4
Since the drawing of the tree in (1) suggests the back of a skeleton, we use ‘spine’ for the central part, or backbone, of the tree.
 
5
In the following, iff means if and only if.
 
6
Following [18, Sect. 1.1], these sets can be empty.
 
7
As in [18], we use ‘structure’ and reserve the word ‘model’ to refer to those structures satisfying a given set of sentences (theory).
 
8
We use ‘hook’ because this formula is intended to ‘catch’ the head of the next inference rule in the spine.
 
9
This transformation keeps no information about the matrix formula \(F\) in the universally quantified formula \((\forall x:s)\,F\). This could compromise the success of its use with Theorem 4 below. More precise transformations could be obtained by considering constants \(c_{x,F}\) indexed not only by variables x but also by formulas \(F\) and envisaging appropriate conditions on such constants so that stability holds.
 
Literature
1.
Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with MU-TERM. In: Proceedings of AMAST’10, LNCS, vol. 6486, pp. 201–208, Springer (2011)
2.
Aguirre, L., Martí-Oliet, N., Palomino, M., Pita, I.: Sentence-normalized conditional narrowing modulo in rewriting logic and Maude. J. Automat. Reason. 60(4), 421–463 (2018)MathSciNetCrossRef
3.
Arts, T., Giesl, J.: Proving innermost normalisation automatically. In: Proceedings of RTA’97, LNCS, vol. 1232, pp. 157–171, Springer, Berlin (1997)CrossRef
4.
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000)MathSciNetCrossRef
5.
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)CrossRef
6.
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude—A High-Performance Logical Framework. LNCS, vol. 4350, Springer (2007)
7.
Durán, F., Lucas, S., Meseguer, J.: Methods for proving termination of rewriting-based programming languages by transformation. Electron. Notes Theor. Comput. Sci. 248, 93–113 (2009)CrossRef
8.
Durán, F., Lucas, S., Marché, C., Meseguer, J., Urbain, X.: Proving operational termination of membership equational programs. High. Order Symb. Comput. 21(1–2), 59–88 (2008)CrossRef
9.
Falke, S., Kapur, D.: Operational termination of conditional rewriting with built-in numbers and semantic data structures. Electron. Notes Theor. Comput. Sci. 237, 75–90 (2009)CrossRef
10.
11.
Giesl, J., Arts, T.: Verification of Erlang processes by dependency pairs. Appl. Algebra Eng. Commun. Comput. 12, 39–72 (2001)MathSciNetCrossRef
12.
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reason. 37(3), 155–203 (2006)MathSciNetCrossRef
13.
Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: combining techniques for automated termination proofs. In: Proceedings of LPAR’04, LNAI, vol. 3452, pp. 301–331 (2004)CrossRef
14.
Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Proceedings of IJCAR’06, LNAI, vol. 4130, pp. 281–286 (2006)
15.
Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Proceedings of TAPSOFT’87, LNCS, vol. 250, pp. 1–22 (1987)
16.
Goguen, J., Meseguer, J.: Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theor. Comput. Sci. 105, 217–273 (1992)MathSciNetCrossRef
17.
Gutiérrez, R., Lucas, S., Reinoso, P.: A tool for the automatic generation of logical models of order-sorted first-order theories. In: Proceedings of PROLE’16, pp. 215–230 (2016)
18.
19.
Korp, M., Sternagel, C., Zankl, H., Middeldorp, A.: Tyrolean termination tool 2. In: Proceedings of RTA 2009, LNCS, vol. 5595, pp. 295–304 (2009)CrossRef
20.
Lalement, R.: Computation as Logic. Masson-Prentice Hall International, Paris (1993)MATH
21.
22.
Lucas, S.: Use of logical models for proving operational termination in general logics. In: Selected Papers from WRLA’16, LNCS, vol. 9942, pp. 1–21 (2016)
23.
24.
Lucas, S., Gutiérrez, R.: Automatic synthesis of logical models for order-sorted first-order theories. J. Autom. Reason. 60(4), 465–501 (2018)MathSciNetCrossRef
25.
Lucas, S., Gutiérrez, R.: Use of logical models for proving infeasibility in term rewriting. Inf. Process. Lett. 136, 90–95 (2018)MathSciNetCrossRef
26.
Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95, 446–453 (2005)MathSciNetCrossRef
27.
Lucas, S., Meseguer, J.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebr. Methods Program. 86, 236–268 (2017)MathSciNetCrossRef
28.
Lucas, S., Meseguer, J.: Proving operational termination of declarative programs in general logics. In: Proceedings of PPDP’14, pp. 111–122. ACM Digital Library (2014)
29.
30.
Mendelson, E.: Introduction to Mathematical Logic, 4th edn. Chapman & Hall, London (1997)MATH
31.
Meseguer, J.: General logics. In: Logic Colloquium’87, pp. 275–329 (1989)
32.
O’Donnell, M.J.: Equational Logic as a Programming Language. The MIT Press, Cambridge (1985)MATH
33.
34.
Prawitz, D.: Natural Deduction. A Proof Theoretical Study. Almqvist & Wiksell, 1965. Reprinted by Dover Publications (2006)
35.
Rosu, G., Stefanescu, A., Ciobaca, S., Moore, B.M.: One-path reachability logic. In: Proceedings of LICS 2013, pp. 358–367. IEEE Press (2013)
36.
Shapiro, S.: Foundations Without Foundationalism: A Case for Second-Order Logic. Clarendon Press, Oxford (1991)MATH
37.
Schernhammer, F., Gramlich, B.: Characterizing and proving operational termination of deterministic conditional term rewriting systems. J. Log. Algebr. Program. 79, 659–688 (2010)MathSciNetCrossRef
38.
Serbanuta, T., Rosu, G.: Computationally equivalent elimination of conditions. In: Proceedings of RTA’06, LNCS, vol. 4098, pp. 19–34. Springer, Berlin (2006)
39.
Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, Univ. Math. Lab., Cambridge, pp. 67–69 (1949)
Metadata
Title
Using Well-Founded Relations for Proving Operational Termination
Author
Salvador Lucas
Publication date
11-02-2019
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-019-09514-2

Premium Partner

    Image Credits