是否有一个完善的Coq图库用于证明简单定理？
我想学习如何证明简单的东西:"G1,G2是同构的,当且仅当它们的补语是同构的"时.
是否有相关/类似的示例或教程？
我正在测试Java 8的新闭包功能; 我想知道为什么这段代码
public class Test8 {
private class A { int a;}
private class B { int b;}
interface IFA { void ifa(A param); }
interface IFB { void ifb(B param); }
private void forceA(A expr) { }
private void z(IFA fun) { System.out.println( "A"); fun.ifa( new A() ); }
private void z(IFB fun) { System.out.println( "B"); fun.ifb( new B() ); }
public void run() {
z( x -> forceA(x) );
}
public static void main(String args[]) { new …关于Coq(使用Init库)的一个非常基本的问题:术语10是类型nat,并且类型nat是归纳定义的:
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
Q1.但"10"是"捷径" S(S(...S(0)...))吗？
Q2.是否有以下引理的最短(正式)证明？(不使用欧米茄)
Lemma gg : 3 <= 10.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_S.
apply le_n.
Qed.
换句话说,n <= m(只有Peano公理)证明需要指数长度吗？
我对Clingo(和逻辑编程)完全陌生,我正在寻找实现以下基本约束的最佳方法:
Q1.我有一个谓词selected(T),其中T的范围从1到N = 5; 如何指定存在至少一个T这样选择(T)？
Q2.我有一个二元谓词wrap(E,T),其中E,T的范围从1到M,N; 如何指定每个E至少存在一个T这样包裹(E,T)？
Q3.我怎么可以指定,如果selected(a)OR selected(b)那么selected(c)一定是假的
我实际上使用了两行代码,但可能有更好的方法:
:- selected(c), selected(a) .
:- selected(c), selected(b) .
Q4.如何指定如果某个条件C(A)为真,则两个一元谓词p1(A)和p2(A)必须具有相同的值？
我实际上使用两行代码:
p1(A) :- C(A), p2(A)
:- C(A), not p2(A), p1(A)
Q5.你建议哪一本书能够很好地介绍答案集编程？