教室：H3409
讲座课：每周四 13:30-15:10
讨论课：双周四 15:25-17:05
幻灯片01 幻灯片02 类型论01 幻灯片03 幻灯片04 幻灯片05 幻灯片06 幻灯片07 幻灯片08 幻灯片09
提交你的作业：https://www.logicbench.cn/
简单的LaTeX符号与公式
- 所有的（行内）公式都应该被两个
$包裹，例如$P\vee Q$会被渲染成 \(P\vee Q\) - 常用的命题逻辑符号
- \(\neg\)：
\neg - \(\vee\)：
\vee - \(\wedge\)：
\wedge - \(\rightarrow\)：
\rightarrow - \(\leftrightarrow\)：
\leftrightarrow - \(\forall\)：
\forall - \(\exists\)：
\exists
- \(\neg\)：
如何提交谓词逻辑的形式化
- 能以命题逻辑的形式提交尽量以命题逻辑提交
- 提交谓词逻辑推理时，Propositional 选择“否”
- Parameters 中输入首字母大写表示谓词，首字母小写表示常元
- 翻译部分要规定参数中列举的：
- 谓词的翻译，如 \(Lxy\) 翻译为“\(x\) 大于 \(y\)”（也暗示了 \(L\) 是二元谓词）
- 常元的翻译，如 a 翻译为“张三”
- Premise、Conclusion 中的公式凡涉及量词必须以“受限量词”的形式出现，例如：\(\exists x(\varphi (x) \rightarrow \psi(x))\)、\(\forall x(\varphi (x) \rightarrow \exists y(\psi(y) ∧ \chi(x, y)))\) （\(\varphi, \psi, \chi\) 是元语言中指代公式的符号）
如何提交成功“骗过 LLM”的证据?
使用主流提供商的官方分享公开链接功能，在“模型回答”中填写公开链接。
可接受的模型提供商
（均关闭思考、联网模式）
一个后台数据的例子
{
"id": 3,
"title": "3x3数独求解",
"original": {
"background": "考虑3*3的数独。规则是每一格中只能填1、2、3中的一个数字，每一行每一列都不能出现重复的数字。目前第一行第一格里是1，第二行第三格里是2",
"question": "右上角（第一行第三格）填什么？",
"answer": "填3"
},
"formalization": [
{
"language": {
"propositional" : true,
"parameters": ["P","Q","R"]
},
"translation": {
"P": "填1",
"Q": "填2",
"R": "填3"
},
"reasoning": {
"premise": [
"$P \vee Q \vee R$",
"$\neg P$",
"$\neg Q$"
],
"conclusion": "$R$"
}
},
{
"language":{
"propositional":true,
"parameters":["P[3,3,3]"] //3表示集合{0,1,2}, P[3, 3, 3]表示：{P_{000},P_{001},\dots,P_{222}}
},
"translation":{
"P_{i.3 j.3 k.3}" : "第$i+1$行第$j+1$格填$k+1$"
},
"reasoning":{
"premise":[
{ //如果是公式模式的话
"index" : ["i.3", "j.3"],
"formula" : "$(P_{i,j,0}\wedge\neg P_{i,j,1}\wedge\neg P_{i,j,2})\vee(\neg P_{i,j,0}\wedge P_{i,j,1}\wedge\neg P_{i,j,2})\vee(\neg P_{i,j,0}\wedge\neg P_{i,j,1}\wedge P_{i,j,2})$"//每个格子填1-3
},
{
"index": ["i1.3", "j1.3", "i2.(3-{i1})", "j2.(3-{j1})", "k.3"],
"formula": "$(P_{i1,j1,k}\rightarrow\neg P_{i1,j2,k})\wedge (P_{i1,j1,k}\rightarrow\neg P_{i2,j1,k})$"//同行、同列不能填同样的数字
},
"P_{1,1,1}",//第1行第1格填1
"P_{2,3,2}"//第2行第3格填2
],
"conclusion": "P_{1,3,3}"
}
}
]
}