AMLOG : an Amalgamated Equational Logic Programming Language

この論文をさがす

抄録

AMLOG is an equational logic programming language based on the concept introduced by Fribourg [6]. In this language an amalgamation of logic programming and equational programming is achieved by combining in the computation procedure the capability of inferring solutions by means of goal reduction as in logic programming and the term rewriting feature of equational programming. The logical basis of equational logic programming languages is established using deductive reasoning about programs. Two deductive systems are proposed the notions of confluence and Church-Rosser property of programs are introduced based on these deductive systems and their equivalence is proved. It is shown that solutions obtained by executing an equational logic program are deducible from the program in the deductive system for equational definite clauses. This result gives the soundness of the computation mechanism. The converse of this result is not true in general. However for confluent programs we have shown the following completeness result: if a goal has a solution deducible from a confluent program under certain conditions then there is a successfully terminating computation for the goal with a more general solution. Some implementation issues and features of the language are discussed.

AMLOG is an equational logic programming language based on the concept introduced by Fribourg [6]. In this language, an amalgamation of logic programming and equational programming is achieved by combining, in the computation procedure, the capability of inferring solutions by means of goal reduction as in logic programming and the term rewriting feature of equational programming. The logical basis of equational logic programming languages is established using deductive reasoning about programs. Two deductive systems are proposed, the notions of confluence and Church-Rosser property of programs are introduced based on these deductive systems, and their equivalence is proved. It is shown that solutions obtained by executing an equational logic program are deducible from the program in the deductive system for equational definite clauses. This result gives the soundness of the computation mechanism. The converse of this result is not true in general. However, for confluent programs, we have shown the following completeness result: if a goal has a solution deducible from a confluent program, under certain conditions, then there is a successfully terminating computation for the goal with a more general solution. Some implementation issues and features of the language are discussed.

収録刊行物

詳細情報

  • CRID
    1050564287846748416
  • NII論文ID
    110002673475
  • NII書誌ID
    AA00700121
  • ISSN
    18826652
  • Web Site
    http://id.nii.ac.jp/1001/00059795/
  • 本文言語コード
    en
  • 資料種別
    article
  • データソース種別
    • IRDB
    • CiNii Articles

問題の指摘

ページトップへ