First-order unification using variable-free relational algebra *

被引:2
|
作者
Gallego Arias, Emilio Jesus [1 ]
Lipton, James [2 ]
Marino, Julio [1 ]
Nogueira, Pablo [1 ]
机构
[1] Univ Politecn Madrid, E-28040 Madrid, Spain
[2] Wesleyan Univ, Middletown, CT 06459 USA
关键词
Unification; Relation Calculus; Rewriting; Abstract Syntax; HIGHER-ORDER UNIFICATION; LOGIC;
D O I
10.1093/jigpal/jzq011
中图分类号
O29 [应用数学];
学科分类号
070104 ;
摘要
We present a framework for the representation and resolution of first-order unification problems and their abstract syntax in a variable-free relational formalism which is an executable variant of the Tarski-Givant relation algebra and of Freyd's allegories restricted to the fragment necessary to compile and run logic programs. We develop a decision procedure for validity of relational terms, which corresponds to solving the original unification problem. The decision procedure is carried out by a conditional relational-term rewriting system. There are advantages over classical unification approaches. First, cumbersome and underspecified meta-logical procedures (name clashes, substitution, etc.) and their properties (invariance under substitution of ground terms, equality's congruence with respect to term forming, etc.) are captured algebraically within the framework. Second, other unification problems can be accommodated, for example, existential quantification in the logic can be interpreted as a new operation whose effect is to formalize the costly and error prone handling of fresh names (renaming apart).
引用
收藏
页码:790 / 820
页数:31
相关论文
共 50 条
  • [1] A Universal Algebra for the Variable-Free Fragment of RCdel
    Beklemishev, Lev D.
    LOGICAL FOUNDATIONS OF COMPUTER SCIENCE (LFCS 2018), 2018, 10703 : 91 - 106
  • [2] Binding of Relational Nouns and the Variable-Free Semantics
    Nakamura, Hiroaki
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2011, 6797 LNAI : 60 - 74
  • [3] First-order unification by structural recursion
    McBride, C
    JOURNAL OF FUNCTIONAL PROGRAMMING, 2003, 13 : 1061 - 1075
  • [4] First-order unification by structural recursion
    Department of Computer Science, University of Durham, South Road, Durham DH1 3LE, United Kingdom
    J. Funct. Program., 1600, 6 (1061-1075):
  • [5] First-Order Unification on Compressed Terms
    Gascon, Adria
    Maneth, Sebastian
    Ramos, Lander
    22ND INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'11), 2011, 10 : 51 - 60
  • [6] Consistency of variable splitting in free variable systems of first-order logic
    Antonsen, R
    Waaler, A
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 2005, 3702 : 33 - 47
  • [7] Relational contracts and the first-order approach
    Hwang, Sunjoo
    JOURNAL OF MATHEMATICAL ECONOMICS, 2016, 63 : 126 - 130
  • [8] Unification in first-order transitive modal logic
    Dzik, Wojciech
    Wojtylak, Piotr
    LOGIC JOURNAL OF THE IGPL, 2019, 27 (05) : 693 - 717
  • [9] First-order unification in the PVS proof assistant
    Avelar, Andreia Borges
    Galdino, Andre Luiz
    Cavalcanti de Moura, Flavio Leonardo
    Ayala-Rincon, Mauricio
    LOGIC JOURNAL OF THE IGPL, 2014, 22 (05) : 758 - 789
  • [10] Toward a First-Order Extension of Prolog's Unification using CHR
    Djelloul, Khalil
    Dao, Thi-Bich-Hanh
    Fruehwirth, Thom
    APPLIED COMPUTING 2007, VOL 1 AND 2, 2007, : 58 - +