TY - GEN
T1 - Models for logics and conditional constraints in automated proofs of termination
AU - Lucas, Salvador
AU - Meseguer, José
N1 - Publisher Copyright:
© Springer International Publishing Switzerland 2014.
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
KW - Conditional constraints
KW - Program analysis
KW - Termination
UR - http://www.scopus.com/inward/record.url?scp=84917678163&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84917678163&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-13770-4_3
DO - 10.1007/978-3-319-13770-4_3
M3 - Conference contribution
AN - SCOPUS:84917678163
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 9
EP - 20
BT - Artificial Intelligence and Symbolic Computation - 12th International Conference, AISC 2014, Proceedings
A2 - Aranda-Corral, Gonzalo A.
A2 - Calmet, Jacques
A2 - Martín-Mateos, Francisco J.
PB - Springer
T2 - 12th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2014
Y2 - 11 December 2014 through 13 December 2014
ER -