Blog

Submit your Logic Translation Homework: https://logic.fudan.edu.cn/logictranslation

Some LaTeX Logic Symbols

• \(\neg\)：\neg or \lnot
• \(\vee\)：\vee or \lor
• \(\wedge\)：\wedge or \land
• \(\rightarrow\)：\rightarrow or \to
• \(\leftrightarrow\)：\leftrightarrow
• \(\forall\)：\forall
• \(\exists\)：\exists

教室：H3409
讲座课：每周四 13:30-15:10
讨论课：双周四 15:25-17:05

幻灯片01 幻灯片02 类型论01 幻灯片03 幻灯片04 幻灯片05 幻灯片06 幻灯片07 幻灯片08 幻灯片09 幻灯片10 幻灯片11 幻灯片12 幻灯片 13（习题）幻灯片 14（习题）

提交你的作业：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

如何提交谓词逻辑的形式化

• 能以命题逻辑的形式提交尽量以命题逻辑提交
• 提交谓词逻辑推理时，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”的证据?

使用主流提供商的官方分享公开链接功能，在“模型回答”中填写公开链接。

可接受的模型提供商

（均关闭思考、联网模式）

• DeepSeek
• Qwen
• Doubao
• ChatGPT

使用Lean判断命题逻辑推理有效性：例子

一个后台数据的例子

{
    "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}"
        }

      }
    ]
  }

Slides 01 Slides 02 Slides 03 Slides 04 Slides 05 Slides 06 Slides 07 Slides 08 Slides 09 Slides 10 Slides 11 Slides 12 Slides 13 Slides 14