如何实现一个将命题公式转换为正常形式的谓词?

huangapple go评论45阅读模式
英文:

How can I implement a predicate which converts a propositional formula to a normal form?

问题

I am trying to implement an unfold predicate which takes a propositional formula and returns one where the only logical operators are conjunction, disjunction and negation.

Code:

:- op(1060, yfx, <->). 
:- op(1050, yfx, <-). 
:- op(800, yfx, xor).
:- op(600, yfx, v).  
:- op(400, yfx, &). 
:- op(200, fy, ¬). 

define((F xor G),  ¬ (F <-> G)).
define((F <-> G), (F -> G) & (F <- G)). 
define((F <- G), (G -> F)).
define((F -> G), ¬ F v G).

% Base case: atomic formula
unfold(A, A) :- atom(A).
unfold(¬ A, NA) :- unfold(A, UA), define(UA, NA1), NA = ¬ NA1.
unfold(A & B, C) :- unfold(A, UA), unfold(B, UB), define(UA, C1), define(UB, C2), C = C1 & C2.
unfold(A v B, C) :- unfold(A, UA), unfold(B, UB), define(UA, C1), define(UB, C2), C = C1 v C2.
unfold(A xor B, C) :- unfold(A, UA), unfold(B, UB), define((UA xor UB), C).
unfold(A <-> B, C) :- unfold(A, UA), unfold(B, UB), define((UA <-> UB), C).
unfold(A <- B, C) :- unfold(A, UA), unfold(B, UB), define((UA <- UB), C).
unfold(A -> B, C) :- unfold(A, UA), unfold(B, UB), define((UA -> UB), C).

However, that doesn't work. At first I missed the base case, then I added it but I only get false. For example, this query should return:

-? unfold( p <-> q & ¬ r, G ).
G= ( ¬p v ¬q & ¬r) & ( ¬ (q & ¬ r) v p). 

Thank you for any guidance or help.

英文:

I am trying to implement an unfold predicate which takes a propositional formula and returns one where the only logical operators are conjunction, disjunction and negation.

Code:

:- op(1060, yfx, <->). 
:- op(1050, yfx, <-). 
:- op(800, yfx, xor).
:- op(600, yfx, v).  
:- op(400, yfx, &). 
:- op(200, fy, ¬). 

define((F xor G),  ¬ (F <-> G)).
define((F <-> G), (F -> G) & (F <- G)). 
define((F <- G), (G -> F)).
define((F -> G), ¬ F v G).

% Base case: atomic formula
unfold(A, A) :- atom(A).
unfold(¬ A, NA) :- unfold(A, UA), define(UA, NA1), NA = ¬ NA1.
unfold(A & B, C) :- unfold(A, UA), unfold(B, UB), define(UA, C1), define(UB, C2), C = C1 & C2.
unfold(A v B, C) :- unfold(A, UA), unfold(B, UB), define(UA, C1), define(UB, C2), C = C1 v C2.
unfold(A xor B, C) :- unfold(A, UA), unfold(B, UB), define((UA xor UB), C).
unfold(A <-> B, C) :- unfold(A, UA), unfold(B, UB), define((UA <-> UB), C).
unfold(A <- B, C) :- unfold(A, UA), unfold(B, UB), define((UA <- UB), C).
unfold(A -> B, C) :- unfold(A, UA), unfold(B, UB), define((UA -> UB), C).

However, that doesn't work. At first I missed the base case, then I added it but I only get false. For example, this query should return:

-? unfold( p <-> q & ¬ r, G ).
G= ( ¬p v ¬q & ¬r) & ( ¬ (q & ¬ r) v p). 

Thank you for any guidance or help.

答案1

得分: 2

当我运行你的程序时,尝试执行unfold(~r, NA)时失败,因为它在define(r, NA1)上失败。看起来,针对原子的定义还没有被编写。我正在使用SWI-PROLOG,并使用gtrace进行调试;这就是我发现故障的方式。

解决方案:编写define/2来处理原子。当然,还可能缺少其他子句。

英文:

When I run your program, it fails when trying unfold(~r, NA), because it fails on define(r, NA1). It seems that define for an atom hasn't been written. I use SWI-PROLOG and am using gtrace for debugging; that's how I found the fault.

Solution: write define/2 to handle atoms. There may of course be other missing clauses.

huangapple
  • 本文由 发表于 2023年4月20日 07:04:37
  • 转载请务必保留本文链接:https://go.coder-hub.com/76059427.html
匿名

发表评论

匿名网友

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen:

确定