我一直在使用以下数据结构来表示Haskell中的命题逻辑:
data Prop
= Pred String
| Not Prop
| And Prop Prop
| Or Prop Prop
| Impl Prop Prop
| Equiv Prop Prop
deriving (Eq, Ord)
欢迎对此结构发表任何评论.
但是,现在我想扩展我的算法来处理FOL - 谓词逻辑.什么是在Haskell中代表FOL的好方法？
我见过的版本 - 几乎是 - 上面的扩展,以及基于更经典的无上下文语法的版本.有没有关于此的文献,可以推荐吗？
haskell context-free-grammar first-order-logic data-structures
关于一阶逻辑中谓词和函数之间的区别,我最近一直很困惑.
到目前为止我的理解是,
谓词是显示比较或显示两个对象之间的关系,如,
President(Obama, America)
函数用于指定特定对象的内容,例如
Human(Obama)
现在我正在走上正确的道路来区分这两个术语,或者我完全错了,需要一个简短的解释,我希望得到专家的意见来澄清我的知识(或批准我的理解).提前致谢
克里奥尔语
algorithm logic artificial-intelligence agent first-order-logic
我现在正在学习一阶逻辑.我正在看这个例子:
一些狗吠∃x(狗(X)Λ树皮(x))
所有的狗都有四条腿∀x(狗(x) - > have_four_legs(x))
我的问题是:第二个例子是否可能是:∀x(dog(x)Λhas_four_legs(x))
为什么第一个例子不能是:∃x(dog(X) - > bark(x))
我正在阅读关于Coq的教程.它构造一个bool类型如下:
Coq < Inductive bool : Set := true | false.
bool is defined
bool_rect is defined
bool_ind is defined
bool_rec is defined
然后它显示了这些东西正在使用"检查".
Coq < Check bool_ind.
bool_ind
: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
Coq < Check bool_rec.
bool_rec
: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
Coq < Check bool_rect.
bool_rect
: …在研究描述逻辑(DL)时,很常见的是它是一阶逻辑(FOL)的一个片段,但很难从DL中排除的内容中明确地读出一些内容,这是FOL的一部分,这使得DL (所有方言ALC,SHOIN等......)可判定.或者换句话说,你能否在FOL中提供一些不能通过DL表达的例子(这是FOL中半/非可判定性的原因)？
早上好,我想了解如何使用一阶逻辑描述一些东西.
例如,我想描述一部电影(实体)是什么,以及电影的属性(例如演员:克鲁尼)是什么.如何使用一阶逻辑描述？
*******更新********
我需要在第一个逻辑顺序中解释的是:
ENTITY:可以使用一组属性或属性描述的元素,抽象或对象.所以我认为我必须说实体有一组具有各自值的属性.实体描述元素,抽象或对象.
属性:属性总是有一个值,它总是与实体相关联.它描述了实体的特定功能/属性.
文档:纯文本描述(纯文本不包含任何html标签).每个文档仅通过其属性描述一个实体.
Monadic一阶逻辑，其中所有谓词都恰好采用一个参数，是一阶逻辑的已知可判定片段。测试公式是否可以满足此逻辑是可以确定的，并且存在基于分辨率的方法来确定这一点。
我处于需要测试一些单子一阶逻辑语句的可满足性的情况。我意识到我将达到理论上的复杂性极限，但我希望在常见情况下能够获得合理的性能。
现在，存在大量的定理证明，它们提供了解决一阶逻辑问题的快速方法。其中包括Vampire，SPASS，E，以及Z3和CVC4的量词扩展。但是，由于不确定性，不能保证它们停止运行。
我的问题
在现有的定理证明者中，有谁能保证在给定单子式公式作为输入时停止？还是有一种方法可以使用它们（以某种方式）有效地测试单子公式的可满足性？
formal-verification proof theorem-proving first-order-logic smt
我开始看Mercury语言,这看起来非常有趣.我是逻辑编程的新手,但在Scala和Haskell中使用函数式编程非常有经验.我一直在思考的一件事是,当你已经拥有至少与类型一样富有表现力的谓词时,为什么你需要逻辑编程中的类型.
例如,在以下代码段中使用类型有什么好处(取自Mercury教程):
:- type list(T) ---> [] ; [T | list(T)].
:- pred fib(int::in, int::out) is det.
fib(N, X) :-
( if N =< 2
then X = 1
else fib(N - 1, A), fib(N - 2, B), X = A + B
).
与仅使用谓词编写它相比:
list(T, []).
list(T, [H | X]) :- T(H), list(T, X).
int(X) :- .... (builtin predicate)
fib(N, X) :-
int(N),
int(X),
( if N =< 2
then X = 1
else fib(N - 1, A), fib(N …我正在 Prolog 中寻找一种方法、模式或内置功能，我可以用它来返回原因，至少就数据库中的谓词而言。当用户在系统中提出查询时，我试图能够说的不仅仅是“那是错误的”。
例如，假设我有两个谓词。 blue/1如果某物是蓝色，则为真；dog/1如果某物是狗，则为真：
blue(X) :- ...
dog(X) :- ...
如果我向 Prolog 提出以下查询并且foo是一只狗，但不是蓝色，Prolog 通常只会返回“false”：
? blue(foo), dog(foo)
false.
我想要的是找出为什么谓词的合取不正确，即使它是带外调用，例如：
? getReasonForFailure(X)
X = not(blue(foo))
如果谓词必须以某种方式编写，我没关系，我只是在寻找人们使用过的任何方法。
迄今为止，我完成此操作并取得了一些成功的方法是以程式化的方式编写谓词，并使用一些辅助谓词来找出事后的原因。例如：
blue(X) :-
recordFailureReason(not(blue(X))),
isBlue(X).
然后实现 recordFailureReason/1 ，以便它始终记住堆栈最深处发生的“原因”。如果查询失败，则发生最深的任何失败都会被记录为失败的“最佳”原因。这种启发式方法在许多情况下都出奇地有效，但确实需要仔细构建谓词才能正常工作。
有任何想法吗？我愿意看看 Prolog 之外是否有专为此类分析而设计的谓词逻辑系统。