Models for logics and conditional constraints in automated proofs of termination

Salvador Lucas, Jose Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Reasoning about termination of declarative programs, which are described by means of a computational logic, requires the definition of appropriate abstractions as semantic models of the logic, and also handling the conditional constraints which are often obtained. The formal treatment of such constraints in automated proofs, often using numeric interpretations and (arithmetic) constraint solving, can greatly benefit from appropriate techniques to deal with the conditional (in)equations at stake. Existing results from linear algebra or real algebraic geometry are useful to deal with them but have received only scant attention to date. We investigate the definition and use of numeric models for logics and the resolution of linear and algebraic conditional constraints as unifying techniques for proving termination of declarative programs.

Original languageEnglish (US)
Title of host publicationArtificial Intelligence and Symbolic Computation - 12th International Conference, AISC 2014, Proceedings
EditorsJacques Calmet, Gonzalo A. Aranda-Corral, Francisco J. Martín-Mateos
PublisherSpringer-Verlag
Pages9-20
Number of pages12
ISBN (Electronic)9783319137698
StatePublished - Jan 1 2014
Event12th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2014 - Seville, Spain
Duration: Dec 11 2014Dec 13 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8884
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other12th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2014
CountrySpain
CitySeville
Period12/11/1412/13/14

Keywords

  • Conditional constraints
  • Program analysis
  • Termination

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Models for logics and conditional constraints in automated proofs of termination'. Together they form a unique fingerprint.

  • Cite this

    Lucas, S., & Meseguer, J. (2014). Models for logics and conditional constraints in automated proofs of termination. In J. Calmet, G. A. Aranda-Corral, & F. J. Martín-Mateos (Eds.), Artificial Intelligence and Symbolic Computation - 12th International Conference, AISC 2014, Proceedings (pp. 9-20). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8884). Springer-Verlag.