使用TweetyProject编写FOL Java代码报错：公式未闭合问题求助

问题描述 #

在使用TweetyProject编写一阶逻辑（FOL）Java代码时，执行查询触发IllegalArgumentException: The given formula exists X: (Knows(Alice,X)) is not closed错误，代码及报错信息如下：

代码示例 #

public class SimpleFolExample {
    public static void main(String[] args) throws ParserException, IOException {
        // Create FOL signature
        FolSignature signature = new FolSignature(true);
     // Add sorts
     // Add sorts
        Sort sortPerson = new Sort("Person");
        signature.add(sortPerson);

        // Add constants
        Constant alice = new Constant("Alice", sortPerson);
        Constant bob = new Constant("Bob", sortPerson);
        Constant James = new Constant("James", sortPerson);
        signature.add(alice, bob, James);

        // Add predicates
     // Add predicates
        List<Sort> personPredicateSorts = new ArrayList<>();
        personPredicateSorts.add(sortPerson);
        Predicate person = new Predicate("Person", personPredicateSorts);
        signature.add(person); // Add predicates to the signature

        // Add the 'Knows' predicate (assuming it relates persons)
        List<Sort> knowsPredicateSorts = new ArrayList<>();
        knowsPredicateSorts.add(sortPerson);
        knowsPredicateSorts.add(sortPerson);
        Predicate knows = new Predicate("Knows", knowsPredicateSorts);
        signature.add(knows);
       

        // Display the signature
        System.out.println("Signature: " + signature);

        // Parse formulas using the signature
        FolParser parser = new FolParser();
        parser.setSignature(signature); // Set the FOL signature for the parser

        FolBeliefSet beliefSet = new FolBeliefSet();
        FolFormula f1 = (FolFormula) parser.parseFormula("Knows(Alice, Bob)");
        FolFormula f2 = (FolFormula) parser.parseFormula("Knows(Bob, James)");
        beliefSet.add(f1, f2);
    

        System.out.println("\nParsed Belief Base: " + beliefSet);

        // Use the reasoner to query the knowledge base
        FolReasoner.setDefaultReasoner(new SimpleFolReasoner());
        FolReasoner prover = FolReasoner.getDefaultReasoner();

        FolFormula query = (FolFormula) parser.parseFormula("exists X:(Knows(Alice, X))");


        System.out.println("Query: " + query + "\nResult: " + prover.query(beliefSet, query));
    }
}

报错信息 #

Signature: [_Any = {}, Person = {Bob, Alice, James}], [==(_Any,_Any), /==(_Any,_Any), Person(Person), Knows(Person,Person)], []

Parsed Belief Base: { Knows(Bob,James), Knows(Alice,Bob) }
Exception in thread "main" java.lang.IllegalArgumentException: The given formula exists X: (Knows(Alice,X)) is not closed.
    at org.tweetyproject.logics.fol.reasoner.SimpleFolReasoner.query(SimpleFolReasoner.java:45)
    at org.tweetyproject.logics.fol.examples.SimpleFolExample.main(SimpleFolExample.java:82)

问题定位 #

报错核心原因：

• SimpleFolReasoner要求查询公式必须是闭式（所有变量都被量词绑定，无自由变量）
• 查询公式exists X:(Knows(Alice, X))中的变量X未指定类型，解析后默认属于_Any类型，但Knows谓词要求第二个参数是Person类型，类型不匹配导致TweetyProject无法正确识别X被量词约束，判定公式为非闭式。

解决方法 #

有两种可行修复方案：

方案1：在查询公式中明确变量类型 #

修改查询语句，指定X的类型为Person，确保变量与谓词类型要求匹配：

FolFormula query = (FolFormula) parser.parseFormula("exists X:Person (Knows(Alice, X))");

方案2：设置解析器的默认排序 #

在初始化FolParser后，设置默认排序为Person，让未指定类型的变量自动使用该类型：

FolParser parser = new FolParser();
parser.setSignature(signature);
parser.setDefaultSort(sortPerson); // 添加该行代码

两种方案均可让查询公式被正确解析为闭式，满足SimpleFolReasoner的要求，执行后会返回正确查询结果（true）。

内容的提问来源于stack exchange，提问作者Hamza TAOURIRT