Edit Profile Lucas, Salvador Compute Distance To: Compute Author ID: lucas.salvador Published as: Lucas, S.; Lucas, Salvador External Links: ORCID · dblp Documents Indexed: 75 Publications since 1996, including 4 Books all top 5 Co-Authors 22 single-authored 17 Meseguer Guaita, José 15 Gutiérrez, Raúl 9 Alarcón, Beatriz 9 Alpuente, María 7 Escobar, Santiago 6 Gramlich, Bernhard 5 Hanus, Michael 4 Durán, Francisco 4 Navarro-Marset, Rafael 3 Borralleras, Cristina 3 Rubio, Albert 2 Falaschi, Moreno 2 Fuhs, Carsten 2 Giesl, Jürgen 2 Marché, Claude 2 Rodríguez-Carbonell, Enric 2 Schneider-Kamp, Peter 2 Urbain, Xavier 2 Vidal, Germán 1 Ballis, Demis 1 Comini, Marco 1 Emmes, Fabian 1 Iborra, José 1 Middeldorp, Aart 1 Oliveras, Albert 1 Otto, Carsten 1 Thiemann, René all top 5 Serials 6 Information Processing Letters 4 Information and Computation 4 Journal of Automated Reasoning 4 Electronic Notes in Theoretical Computer Science 2 The Journal of Functional and Logic Programming 2 Theory and Practice of Logic Programming 2 Journal of Logical and Algebraic Methods in Programming 1 Artificial Intelligence 1 Journal of Computer and System Sciences 1 Theoretical Computer Science 1 Applicable Algebra in Engineering, Communication and Computing 1 Higher-Order and Symbolic Computation 1 RAIRO. Theoretical Informatics and Applications Fields 74 Computer science (68-XX) 9 Mathematical logic and foundations (03-XX) 4 General and overarching topics; collections (00-XX) 1 Field theory and polynomials (12-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 61 Publications have been cited 409 times in 132 Documents Cited by ▼ Year ▼ Context-sensitive computations in functional and functional programs. Zbl 0924.68106Lucas, Salvador 36 1998 Proving operational termination of membership equational programs. Zbl 1192.68154Durán, Francisco; Lucas, Salvador; Marché, Claude; Meseguer, José; Urbain, Xavier 30 2008 Operational termination of conditional term rewriting systems. Zbl 1185.68374Lucas, Salvador; Marché, Claude; Meseguer, José 30 2005 Context-sensitive rewriting strategies. Zbl 1012.68095Lucas, Salvador 26 2002 MTT: The Maude termination tool. (System description). Zbl 1165.68360Durán, Francisco; Lucas, Salvador; Meseguer, José 17 2008 Polynomials over the reals in proofs of termination: from theory to practice. Zbl 1085.68076Lucas, Salvador 14 2005 Termination of rewriting with strategy annotations. Zbl 1275.68084Lucas, Salvador 13 2001 Proving termination properties with mu-term. Zbl 1308.68068Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador; Navarro-Marset, Rafael 11 2011 Proving termination of context-sensitive rewriting by transformation. Zbl 1171.68514Lucas, Salvador 11 2006 Recursive path orderings can be context-sensitive. Zbl 1072.68537Borralleras, Cristina; Lucas, Salvador; Rubio, Albert 11 2002 Operational termination of membership equational programs: the order-sorted way. Zbl 1347.68198Lucas, Salvador; Meseguer, José 10 2009 Proving termination of context-sensitive rewriting with MU-TERM. Zbl 1278.68113Alarcón, Beatriz; Gutiérrez, Raúl; Iborra, José; Lucas, Salvador 10 2007 Abstract diagnosis of functional programs. Zbl 1278.68056Alpuente, María; Comini, Marco; Escobar, Santiago; Falaschi, Moreno; Lucas, Salvador 10 2003 Context-sensitive dependency pairs. Zbl 1177.68133Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador 9 2006 Normal forms and normal theories in conditional rewriting. Zbl 1356.68124Lucas, Salvador; Meseguer, José 8 2016 Termination modulo combinations of equational theories. Zbl 1193.68145Durán, Francisco; Lucas, Salvador; Meseguer, José 8 2009 Specialization of functional logic programs based on needed narrowing. Zbl 1092.68018Alpuente, María; Lucas, Salvador; Vidal, Germán; Hanus, Michael 8 2005 Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic. Zbl 1250.68184Borralleras, Cristina; Lucas, Salvador; Navarro-Marset, Rafael; Rodríguez-Carbonell, Enric; Rubio, Albert 7 2009 Search techniques for rational polynomial orders. Zbl 1166.68354Fuhs, Carsten; Navarro-Marset, Rafael; Otto, Carsten; Giesl, Jürgen; Lucas, Salvador; Schneider-Kamp, Peter 7 2008 Strongly sequential and inductively sequential term rewriting systems. Zbl 1339.68136Hanus, Michael; Lucas, Salvador; Middeldorp, Aart 7 1998 A dependency pair framework for \(A \vee C\)-termination. Zbl 1306.68060Alarcón, Beatriz; Lucas, Salvador; Meseguer, José 6 2010 Improving context-sensitive dependency pairs. Zbl 1182.68092Alarcón, Beatriz; Emmes, Fabian; Fuhs, Carsten; Giesl, Jürgen; Gutiérrez, Raúl; Lucas, Salvador; Schneider-Kamp, Peter; Thiemann, René 6 2008 Polynomials for proving termination of context-sensitive rewriting. Zbl 1126.68448Lucas, Salvador 6 2004 Lazy rewriting and context-sensitive rewriting. Zbl 1268.68100Lucas, Salvador 6 2002 Termination of (canonical) context-sensitive rewriting. Zbl 1045.68074Lucas, Salvador 6 2002 Termination of context sensitive rewriting by rewriting. Zbl 1046.68565Lucas, Salvador 6 1996 Automatic synthesis of logical models for order-sorted first-order theories. Zbl 1398.68095Lucas, Salvador; Gutiérrez, Raúl 5 2018 Dependency pairs for proving termination properties of conditional term rewriting systems. Zbl 1353.68155Lucas, Salvador; Meseguer, José 5 2017 2D dependency pairs for proving operational termination of CTRSs. Zbl 1367.68145Lucas, Salvador; Meseguer, José 5 2014 Use of logical models for proving infeasibility in term rewriting. Zbl 06873295Lucas, Salvador; Gutiérrez, Raúl 4 2018 Extending the 2D dependency pair framework for conditional term rewriting systems. Zbl 1457.68136Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl 4 2015 Proving termination in the context-sensitive dependency pair framework. Zbl 1306.68072Gutiérrez, Raúl; Lucas, Salvador 4 2010 Context-sensitive dependency pairs. Zbl 1206.68158Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador 4 2010 Methods for proving termination of rewriting-based programming languages by transformation. Zbl 1337.68067Durán, Francisco; Lucas, Salvador; Meseguer, José 4 2009 Improving the context-sensitive dependency graph. Zbl 1278.68114Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador 4 2007 Transfinite rewriting semantics for term rewriting systems. Zbl 0981.68070Lucas, Salvador 4 2001 Analysis of rewriting-based systems as first-order theories. Zbl 06932830Lucas, Salvador 3 2018 Localized operational termination in general logics. Zbl 1453.68053Lucas, Salvador; Meseguer, José 3 2015 Strong and weak operational termination of order-sorted rewrite theories. Zbl 1367.68144Lucas, Salvador; Meseguer, José 3 2014 SAT modulo linear arithmetic for solving polynomial constraints. Zbl 1243.68210Borralleras, Cristina; Lucas, Salvador; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert 3 2012 Termination of innermost context-sensitive rewriting using dependency pairs. Zbl 1148.68463Alarcón, Beatriz; Lucas, Salvador 3 2007 Removing redundant arguments automatically. Zbl 1112.68068Alpuente, M.; Escobar, S.; Lucas, S. 3 2007 Correct and complete (positive) strategy annotations for OBJ. Zbl 1272.68071Alpuente, María; Escobar, Santiago; Lucas, Salvador 3 2004 Specialization of inductively sequential functional logic programs. Zbl 1345.68090Alpuente, María; Hanus, Michael; Lucas, Salvador; Vidal, Germán 3 1999 Use of logical models for proving operational termination in general logics. Zbl 1367.68068Lucas, Salvador 2 2016 On-demand strategy annotations revisited: an improved on-demand evaluation strategy. Zbl 1186.68092Alpuente, M.; Escobar, S.; Gramlich, B.; Lucas, S. 2 2010 Usable rules for context-sensitive rewrite systems. Zbl 1145.68447Gutiérrez, Raúl; Lucas, Salvador; Urbain, Xavier 2 2008 On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting. Zbl 1103.68061Lucas, Salvador 2 2006 Improving on-demand strategy annotations. Zbl 1023.03530Alpuente, M.; Escobar, S.; Gramlich, B.; Lucas, S. 2 2002 Root-neededness and approximations of neededness. Zbl 1339.68139Lucas, Salvador 2 1998 Using well-founded relations for proving operational termination. Zbl 07176596Lucas, Salvador 1 2020 Automatic generation of logical models with AGES. Zbl 07178982Gutiérrez, Raúl; Lucas, Salvador 1 2019 The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors. Zbl 1393.68088Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl 1 2018 Function calls at frozen positions in termination of context-sensitive rewriting. Zbl 1321.68330Gutiérrez, Raúl; Lucas, Salvador 1 2015 Completeness of context-sensitive rewriting. Zbl 1302.68144Lucas, Salvador 1 2015 Automatic proofs of termination with elementary interpretations. Zbl 1294.68058Lucas, Salvador 1 2009 Termination of just/fair computations in term rewriting. Zbl 1146.68040Lucas, Salvador; Meseguer, José 1 2008 Generalizing Newman’s lemma for left-linear rewrite systems. Zbl 1151.68445Gramlich, Bernhard; Lucas, Salvador 1 2006 Strategies in programming languages today. Zbl 1272.68073Lucas, Salvador 1 2005 Termination of fair computations in term rewriting. Zbl 1143.68491Lucas, Salvador; Meseguer, José 1 2005 An evaluation semantics for narrowing-based functional logic languages. Zbl 0971.68097Hanus, Michael; Lucas, Salvador 1 2001 Using well-founded relations for proving operational termination. Zbl 07176596Lucas, Salvador 1 2020 Automatic generation of logical models with AGES. Zbl 07178982Gutiérrez, Raúl; Lucas, Salvador 1 2019 Automatic synthesis of logical models for order-sorted first-order theories. Zbl 1398.68095Lucas, Salvador; Gutiérrez, Raúl 5 2018 Use of logical models for proving infeasibility in term rewriting. Zbl 06873295Lucas, Salvador; Gutiérrez, Raúl 4 2018 Analysis of rewriting-based systems as first-order theories. Zbl 06932830Lucas, Salvador 3 2018 The 2D dependency pair framework for conditional rewrite systems. I: Definition and basic processors. Zbl 1393.68088Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl 1 2018 Dependency pairs for proving termination properties of conditional term rewriting systems. Zbl 1353.68155Lucas, Salvador; Meseguer, José 5 2017 Normal forms and normal theories in conditional rewriting. Zbl 1356.68124Lucas, Salvador; Meseguer, José 8 2016 Use of logical models for proving operational termination in general logics. Zbl 1367.68068Lucas, Salvador 2 2016 Extending the 2D dependency pair framework for conditional term rewriting systems. Zbl 1457.68136Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl 4 2015 Localized operational termination in general logics. Zbl 1453.68053Lucas, Salvador; Meseguer, José 3 2015 Function calls at frozen positions in termination of context-sensitive rewriting. Zbl 1321.68330Gutiérrez, Raúl; Lucas, Salvador 1 2015 Completeness of context-sensitive rewriting. Zbl 1302.68144Lucas, Salvador 1 2015 2D dependency pairs for proving operational termination of CTRSs. Zbl 1367.68145Lucas, Salvador; Meseguer, José 5 2014 Strong and weak operational termination of order-sorted rewrite theories. Zbl 1367.68144Lucas, Salvador; Meseguer, José 3 2014 SAT modulo linear arithmetic for solving polynomial constraints. Zbl 1243.68210Borralleras, Cristina; Lucas, Salvador; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert 3 2012 Proving termination properties with mu-term. Zbl 1308.68068Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador; Navarro-Marset, Rafael 11 2011 A dependency pair framework for \(A \vee C\)-termination. Zbl 1306.68060Alarcón, Beatriz; Lucas, Salvador; Meseguer, José 6 2010 Proving termination in the context-sensitive dependency pair framework. Zbl 1306.68072Gutiérrez, Raúl; Lucas, Salvador 4 2010 Context-sensitive dependency pairs. Zbl 1206.68158Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador 4 2010 On-demand strategy annotations revisited: an improved on-demand evaluation strategy. Zbl 1186.68092Alpuente, M.; Escobar, S.; Gramlich, B.; Lucas, S. 2 2010 Operational termination of membership equational programs: the order-sorted way. Zbl 1347.68198Lucas, Salvador; Meseguer, José 10 2009 Termination modulo combinations of equational theories. Zbl 1193.68145Durán, Francisco; Lucas, Salvador; Meseguer, José 8 2009 Solving non-linear polynomial arithmetic via SAT modulo linear arithmetic. Zbl 1250.68184Borralleras, Cristina; Lucas, Salvador; Navarro-Marset, Rafael; Rodríguez-Carbonell, Enric; Rubio, Albert 7 2009 Methods for proving termination of rewriting-based programming languages by transformation. Zbl 1337.68067Durán, Francisco; Lucas, Salvador; Meseguer, José 4 2009 Automatic proofs of termination with elementary interpretations. Zbl 1294.68058Lucas, Salvador 1 2009 Proving operational termination of membership equational programs. Zbl 1192.68154Durán, Francisco; Lucas, Salvador; Marché, Claude; Meseguer, José; Urbain, Xavier 30 2008 MTT: The Maude termination tool. (System description). Zbl 1165.68360Durán, Francisco; Lucas, Salvador; Meseguer, José 17 2008 Search techniques for rational polynomial orders. Zbl 1166.68354Fuhs, Carsten; Navarro-Marset, Rafael; Otto, Carsten; Giesl, Jürgen; Lucas, Salvador; Schneider-Kamp, Peter 7 2008 Improving context-sensitive dependency pairs. Zbl 1182.68092Alarcón, Beatriz; Emmes, Fabian; Fuhs, Carsten; Giesl, Jürgen; Gutiérrez, Raúl; Lucas, Salvador; Schneider-Kamp, Peter; Thiemann, René 6 2008 Usable rules for context-sensitive rewrite systems. Zbl 1145.68447Gutiérrez, Raúl; Lucas, Salvador; Urbain, Xavier 2 2008 Termination of just/fair computations in term rewriting. Zbl 1146.68040Lucas, Salvador; Meseguer, José 1 2008 Proving termination of context-sensitive rewriting with MU-TERM. Zbl 1278.68113Alarcón, Beatriz; Gutiérrez, Raúl; Iborra, José; Lucas, Salvador 10 2007 Improving the context-sensitive dependency graph. Zbl 1278.68114Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador 4 2007 Termination of innermost context-sensitive rewriting using dependency pairs. Zbl 1148.68463Alarcón, Beatriz; Lucas, Salvador 3 2007 Removing redundant arguments automatically. Zbl 1112.68068Alpuente, M.; Escobar, S.; Lucas, S. 3 2007 Proving termination of context-sensitive rewriting by transformation. Zbl 1171.68514Lucas, Salvador 11 2006 Context-sensitive dependency pairs. Zbl 1177.68133Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador 9 2006 On the relative power of polynomials with real, rational, and integer coefficients in proofs of termination of rewriting. Zbl 1103.68061Lucas, Salvador 2 2006 Generalizing Newman’s lemma for left-linear rewrite systems. Zbl 1151.68445Gramlich, Bernhard; Lucas, Salvador 1 2006 Operational termination of conditional term rewriting systems. Zbl 1185.68374Lucas, Salvador; Marché, Claude; Meseguer, José 30 2005 Polynomials over the reals in proofs of termination: from theory to practice. Zbl 1085.68076Lucas, Salvador 14 2005 Specialization of functional logic programs based on needed narrowing. Zbl 1092.68018Alpuente, María; Lucas, Salvador; Vidal, Germán; Hanus, Michael 8 2005 Strategies in programming languages today. Zbl 1272.68073Lucas, Salvador 1 2005 Termination of fair computations in term rewriting. Zbl 1143.68491Lucas, Salvador; Meseguer, José 1 2005 Polynomials for proving termination of context-sensitive rewriting. Zbl 1126.68448Lucas, Salvador 6 2004 Correct and complete (positive) strategy annotations for OBJ. Zbl 1272.68071Alpuente, María; Escobar, Santiago; Lucas, Salvador 3 2004 Abstract diagnosis of functional programs. Zbl 1278.68056Alpuente, María; Comini, Marco; Escobar, Santiago; Falaschi, Moreno; Lucas, Salvador 10 2003 Context-sensitive rewriting strategies. Zbl 1012.68095Lucas, Salvador 26 2002 Recursive path orderings can be context-sensitive. Zbl 1072.68537Borralleras, Cristina; Lucas, Salvador; Rubio, Albert 11 2002 Lazy rewriting and context-sensitive rewriting. Zbl 1268.68100Lucas, Salvador 6 2002 Termination of (canonical) context-sensitive rewriting. Zbl 1045.68074Lucas, Salvador 6 2002 Improving on-demand strategy annotations. Zbl 1023.03530Alpuente, M.; Escobar, S.; Gramlich, B.; Lucas, S. 2 2002 Termination of rewriting with strategy annotations. Zbl 1275.68084Lucas, Salvador 13 2001 Transfinite rewriting semantics for term rewriting systems. Zbl 0981.68070Lucas, Salvador 4 2001 An evaluation semantics for narrowing-based functional logic languages. Zbl 0971.68097Hanus, Michael; Lucas, Salvador 1 2001 Specialization of inductively sequential functional logic programs. Zbl 1345.68090Alpuente, María; Hanus, Michael; Lucas, Salvador; Vidal, Germán 3 1999 Context-sensitive computations in functional and functional programs. Zbl 0924.68106Lucas, Salvador 36 1998 Strongly sequential and inductively sequential term rewriting systems. Zbl 1339.68136Hanus, Michael; Lucas, Salvador; Middeldorp, Aart 7 1998 Root-neededness and approximations of neededness. Zbl 1339.68139Lucas, Salvador 2 1998 Termination of context sensitive rewriting by rewriting. Zbl 1046.68565Lucas, Salvador 6 1996 all cited Publications top 5 cited Publications all top 5 Cited by 147 Authors 34 Lucas, Salvador 26 Meseguer Guaita, José 12 Escobar, Santiago 10 Alpuente, María 10 Middeldorp, Aart 9 Gutiérrez, Raúl 9 Martí-Oliet, Narciso 8 Durán, Francisco 6 Antoy, Sergio 6 Nishida, Naoki 6 Thiemann, René 5 Alarcón, Beatriz 5 Gramlich, Bernhard 5 Hirokawa, Nao 5 Iborra, José 5 Sakai, Masahiko 5 Winkler, Sarah 4 Hanus, Michael 4 Kirchner, Hélène 4 Marché, Claude 4 Ogata, Kazuhiro 4 Talcott, Carolyn L. 4 Vidal, Germán 3 Eker, Steven 3 Endrullis, Jörg 3 Falaschi, Moreno 3 Futatsugi, Kokichi 3 Giesl, Jürgen 3 Nakamura, Masaki 3 Palomino, Miguel 3 Riesco, Adrián 3 Rocha, Camilo 3 Rodríguez-Carbonell, Enric 3 Rubio, Albert 3 Schneider-Kamp, Peter 3 Urbain, Xavier 3 Zankl, Harald 2 Ábrahám, Erika 2 Aguirre, Luis Antonio 2 Borralleras, Cristina 2 Caballero, Rafael E. 2 Comini, Marco 2 Falke, Stephan 2 Fissore, Olivier 2 Fuhs, Carsten 2 Gmeiner, Karl 2 Gnaedig, Isabelle 2 Hendriks, Dimitri 2 Jacquemard, Florent 2 Kop, Cynthia 2 López-Fraguas, Francisco Javier 2 Mossakowski, Till 2 Navarro-Marset, Rafael 2 Ojeda, Pedro 2 Oliveras, Albert 2 Pita, Isabel 2 Sakabe, Toshiki 2 Schernhammer, Felix 2 Verdejo, Alberto 2 Yamada, Akihisa 1 Abbott, John A. 1 Albert, Elvira 1 Aschermann, Cornelius 1 Bacci, Giovanni 1 Ballis, Demis 1 Becker, Bernd 1 Bergenti, Federico 1 Bigatti, Anna Maria 1 Blanqui, Frédéric 1 Bonfante, Guillaume 1 Bouhoula, Adel 1 Brain, Martin 1 Brockschmidt, Marc 1 Brown, Daniel W. 1 Bruni, Roberto 1 Buchberger, Bruno 1 Candeago, Lorenzo 1 Chiang, Su-Hui 1 Cimatti, Alessandro 1 Clavel, Manuel 1 Codescu, Mihai 1 Codish, Michael 1 Contejean, Evelyne 1 Correa, Francisco José 1 Corzilius, Florian 1 Davenport, James Harold 1 de Dios Castro, Javier 1 de Vrijer, Roel 1 Deloup, Florian L. 1 Emmes, Fabian 1 England, Matthew 1 Espert, Javier 1 Fernández, Maribel 1 Fernández, Mirtha-Lina 1 Fontaine, Pascal 1 Forrest, Stephen 1 Frohn, Florian 1 Gaĭnă, Daniel 1 Griggio, Alberto 1 Henrot, Antoine ...and 47 more Authors all top 5 Cited in 21 Serials 16 Theoretical Computer Science 12 Journal of Automated Reasoning 8 Information and Computation 7 Journal of Logical and Algebraic Methods in Programming 5 Information Processing Letters 5 Journal of Symbolic Computation 4 The Journal of Logic and Algebraic Programming 2 Applicable Algebra in Engineering, Communication and Computing 2 Annals of Mathematics and Artificial Intelligence 1 Artificial Intelligence 1 Journal of Computer and System Sciences 1 New Generation Computing 1 Formal Aspects of Computing 1 MSCS. Mathematical Structures in Computer Science 1 Journal of Functional Programming 1 Higher-Order and Symbolic Computation 1 RAIRO. Theoretical Informatics and Applications 1 Theory and Practice of Logic Programming 1 ACM Transactions on Computational Logic 1 Journal of Applied Logic 1 Logical Methods in Computer Science all top 5 Cited in 9 Fields 132 Computer science (68-XX) 24 Mathematical logic and foundations (03-XX) 2 History and biography (01-XX) 2 Operations research, mathematical programming (90-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Field theory and polynomials (12-XX) 1 Algebraic geometry (14-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Category theory; homological algebra (18-XX) Citations by Year