Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude

被引:0
|
作者
Luis Aguirre
Narciso Martí-Oliet
Miguel Palomino
Isabel Pita
机构
[1] Universidad Complutense de Madrid,Facultad de Informática
来源
关键词
Maude; Narrowing; Reachability; Rewriting logic; Membership equational logic; Unification;
D O I
暂无
中图分类号
学科分类号
摘要
This work studies the relationship between verifiable and computable answers for reachability problems in rewrite theories with an underlying membership equational logic. A new definition for R, A-rewriting that allows us to solve a bigger class of reachability problems, and a calculus that solves this class of problems always working with canonical terms and normalized substitutions has been developed. Given a reachability problem in a rewrite theory, this calculus can compute any normalized answer that can be checked by rewriting, or a more general one that can be instantiated to that answer.
引用
收藏
页码:421 / 463
页数:42
相关论文
共 29 条
  • [1] Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
    Palomino, Miguel (miguelpt@ucm.es), 1600, Springer Science and Business Media B.V. (60):
  • [2] Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
    Aguirre, Luis
    Marti-Oliet, Narciso
    Palomino, Miguel
    Pita, Isabel
    LOGIC, REWRITING, AND CONCURRENCY, 2015, 9200 : 48 - 71
  • [3] Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
    Aguirre, Luis
    Marti-Oliet, Narciso
    Palomino, Miguel
    Pita, Isabel
    JOURNAL OF AUTOMATED REASONING, 2018, 60 (04) : 421 - 463
  • [4] Conditional Narrowing Modulo in Rewriting Logic and Maude
    Aguirre, Luis
    Marti-Oliet, Narciso
    Palomino, Miguel
    Pita, Isabel
    REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2014, 2014, 8663 : 80 - 96
  • [5] Confluence of Conditional Rewriting Modulo
    Lucas, Salvador
    32ND EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC, CSL 2024, 2024, 288
  • [6] Maude:: Specification and programming in rewriting logic
    Clavel, M
    Durán, F
    Eker, S
    Lincoln, P
    Martí-Oliet, N
    Meseguer, J
    Quesada, JF
    THEORETICAL COMPUTER SCIENCE, 2002, 285 (02) : 187 - 243
  • [7] Equational Abstractions in Rewriting Logic and Maude
    Marti-Oliet, Narciso
    Duran, Francisco
    Verdejo, Alberto
    FORMAL METHODS: FOUNDATIONS AND APPLICATIONS, SBMF 2014, 2015, 8941 : 17 - 31
  • [8] Rewriting logic and Maude: Concepts and applications
    Meseguer, J
    REWRITING TECHNIQUES AND APPLICATIONS, PROCEEDINGS, 2000, 1833 : 1 - 26
  • [9] CONDITIONAL NARROWING MODULO A SET OF EQUATIONS
    BOCKMAYR, A
    APPLICABLE ALGEBRA IN ENGINEERING COMMUNICATION AND COMPUTING, 1993, 4 (03) : 147 - 168
  • [10] Conditional Narrowing Modulo SMT and Axioms
    Aguirre, Luis
    Marti-Oliet, Narciso
    Palomino, Miguel
    Pita, Isabel
    PROCEEDINGS OF THE 19TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING (PPDP 2017), 2017, : 17 - 28