Article

Free access

Termination detection in logic programs using argument sizes (extended abstract)

Authors:

Kirack Sohn,

Allen Van GelderAuthors Info & Claims

PODS '91: Proceedings of the tenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems

Pages 216 - 226

https://doi.org/10.1145/113413.113433

Published: 01 April 1991 Publication History

PDF eReader

References

[1]

F. Afrati, C. Papadimitriou, G. Papageorgiou, A. R. Roussou, Y. Sagiv, and J. D. Ullman. On the convergence of query evaluation. Journal of Computer and System Sciences, 38(2):341-359, 1989.

Crossref

Google Scholar

[2]

A. Brodsky and Y. Sagiv. Inference of monotonicity constraints in Datalog programs. In Eighth A CM Symposium on Principles of Database Systems, pages 190-199, 1989.

Digital Library

Google Scholar

[3]

A. Brodsky and Y. Sagiv. On termination of Datalog programs. In First International Conference on Deductive and Object- Oriented Databases, pages 95-112, Kyoto, Japan, 1989.

Google Scholar

[4]

A. Brodsky and Y. Sagiv. Inference of inequality constraints in logic programs. In Tenth A CM Symposium on Principles of Database Systems, 1990.

Digital Library

Google Scholar

[5]

B.C. Eaves and U. G. Rothblum. Elimination of quantifiers of linear variables and corresponding transfer principles. Technical Report Operations Research, Stanford University, 1987.

Google Scholar

[6]

J.-L. Lassez. Querying constraints. In N#nth A CM Symposium on Principles of Database Systems, pages 288-298, 1990.

Digital Library

Google Scholar

[7]

J.-L. Lassez, H. Huynh, and K. McAloon. Simplification and elimination of redundant linear arithmetic constraints. In North American Conf. on Logic Programming, pages 37-51, 1989.

Google Scholar

[8]

L. Naish. Automatic generation of control for logic programs. Technical Report 83/6, Dept. of Computer Science, University of Melbourne, Melbourne, Australia, 1983.

Google Scholar

[9]

L. Pliimer. Termination Proofs for Logzc Programs, volume 446 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 1990.

Digital Library

Google Scholar

[10]

C.H. Papadimitriou and K. Steiglitz. Combinatorial Optimization. Prentice-Hall, Englewood Cliffs, NJ, 1982.

Digital Library

Google Scholar

[11]

A. Schrijver. Theory of Linear and Integer Programming. Wiley, New York, 1986.

Digital Library

Google Scholar

[12]

Y. Sagiv and J. D. Ullman. Complexity of a top-down capture rule. Technical Report STAN-CS-84-1009, Stanford University, 1984.

Crossref

Google Scholar

[13]

J.D. Ullman. Implementation of logical query languages for databases. A CM Transactions on Database Systems, 10(3):289-321, 1985.

Digital Library

Google Scholar

[14]

J.D. Ullman and A. Van Gelder. Efficient tests for top-down termination of logical rules. Journal of the A CM, 35(2):345-373, 1988.

Digital Library

Google Scholar

[15]

A. Van Gelder. Deriving constraints among argument sizes in logic programs. Annals of Mathematics and Artificial Intelligence, (to appear), 1990. Available as UCS;C-CRL- 89-41. Extended abstract appears in Ninth ACM Symposium on Principles of Database Systems, 1990.

Digital Library

Google Scholar

[16]

C. Walther. Automated Termination Proofs. PhD thesis, University of Karlsruhe, 1988.

Google Scholar

Cited By

View all

Kafle BGange GSchachte PSøndergaard HStuckey P(2024)A lightweight approach to nontermination inference using Constrained Horn ClausesSoftware and Systems Modeling (SoSyM)10.1007/s10270-024-01161-523:2(319-342)Online publication date: 1-Apr-2024
https://dl.acm.org/doi/10.1007/s10270-024-01161-5
Chatterjee KKafshdar Goharshady ENovotný PZárevúcky JŽikelić Đ(2023)On Lexicographic Proof Rules for Probabilistic TerminationFormal Aspects of Computing10.1145/358539135:2(1-25)Online publication date: 23-Jun-2023
https://dl.acm.org/doi/10.1145/3585391
Douglas Giles RPotanin A(2022)Termination of Recursive Functions by Lexicographic Orders of Linear CombinationsCompanion Proceedings of the 2022 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity10.1145/3563768.3563958(75-77)Online publication date: 29-Nov-2022
https://dl.acm.org/doi/10.1145/3563768.3563958
Show More Cited By

Index Terms

Termination detection in logic programs using argument sizes (extended abstract)

Recommendations

Abstract Relations Between Restricted Termination And Confluence Properties Of Rewrite Systems

We investigate restricted termination and confluence properties of term rewriting systems, in particular weak termination, weak innermost termination, (strong) innermost termination, (strong) termination, and their interrelations. New criteria are ...
Termination prediction for general logic programs

We present a heuristic framework for attacking the undecidable termination problem of logic programs, as an alternative to current termination/nontermination proof approaches. We introduce an idea of termination prediction, which predicts termination of ...
Termination prediction for general logic programs

We present a heuristic framework for attacking the undecidable termination problem of logic programs, as an alternative to current termination/nontermination proof approaches. We introduce an idea of termination prediction, which predicts termination of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

PODS '91: Proceedings of the tenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems

April 1991

341 pages

ISBN:0897914309

DOI:10.1145/113413

Chairman:
Daniel J. Rosenkrantz
State Univ. of New York, Albany

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 April 1991

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

SIGMOD/PODS91

Sponsor:

SIGMOD/PODS91: SIGMOD/PODS 91

May 29 - 31, 1991

Colorado, Denver, USA

Acceptance Rates

Overall Acceptance Rate 642 of 2,707 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

59
Total Citations
View Citations
346
Total Downloads

Downloads (Last 12 months)52
Downloads (Last 6 weeks)10

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Kafle BGange GSchachte PSøndergaard HStuckey P(2024)A lightweight approach to nontermination inference using Constrained Horn ClausesSoftware and Systems Modeling (SoSyM)10.1007/s10270-024-01161-523:2(319-342)Online publication date: 1-Apr-2024
https://dl.acm.org/doi/10.1007/s10270-024-01161-5
Chatterjee KKafshdar Goharshady ENovotný PZárevúcky JŽikelić Đ(2023)On Lexicographic Proof Rules for Probabilistic TerminationFormal Aspects of Computing10.1145/358539135:2(1-25)Online publication date: 23-Jun-2023
https://dl.acm.org/doi/10.1145/3585391
Douglas Giles RPotanin A(2022)Termination of Recursive Functions by Lexicographic Orders of Linear CombinationsCompanion Proceedings of the 2022 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity10.1145/3563768.3563958(75-77)Online publication date: 29-Nov-2022
https://dl.acm.org/doi/10.1145/3563768.3563958
Kafle BGallagher JHermenegildo MKlemen MLópez-García PMorales J(2021)Regular Path Clauses and Their Application in Solving LoopsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.344.3344(22-35)Online publication date: 13-Sep-2021
https://doi.org/10.4204/EPTCS.344.3
Domenech JGenaim S(2021)Termination Analysis of Programs with Multiphase Control-FlowElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.344.2344(13-21)Online publication date: 13-Sep-2021
https://doi.org/10.4204/EPTCS.344.2
Chatterjee KGoharshady ENovotný PZárevúcky JŽikelić Đ(2021)On Lexicographic Proof Rules for Probabilistic TerminationFormal Methods10.1007/978-3-030-90870-6_33(619-639)Online publication date: 20-Nov-2021
https://dl.acm.org/doi/10.1007/978-3-030-90870-6_33
Chatterjee KFu HGoharshady A(2019)Non-polynomial Worst-Case Analysis of Recursive ProgramsACM Transactions on Programming Languages and Systems10.1145/333998441:4(1-52)Online publication date: 12-Oct-2019
https://dl.acm.org/doi/10.1145/3339984
Wang PFu HGoharshady AChatterjee KQin XShi WMcKinley KFisher K(2019)Cost analysis of nondeterministic probabilistic programsProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314581(204-220)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314581
Li YSun XLi YTurrini AZhang L(2019)Synthesizing Nested Ranking Functions for Loop Programs via SVMFormal Methods and Software Engineering10.1007/978-3-030-32409-4_27(438-454)Online publication date: 5-Nov-2019
https://dl.acm.org/doi/10.1007/978-3-030-32409-4_27
Ben-Amram ADoménech JGenaim S(2019)Multiphase-Linear Ranking Functions and Their Relation to Recurrent SetsStatic Analysis10.1007/978-3-030-32304-2_22(459-480)Online publication date: 8-Oct-2019
https://dl.acm.org/doi/10.1007/978-3-030-32304-2_22
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Abstract Relations Between Restricted Termination And Confluence Properties Of Rewrite Systems

Termination prediction for general logic programs

Termination prediction for general logic programs