Skip to content

TPTP Compiler

Bases: Compiler

Source code in src/typedlogic/compilers/tptp_compiler.py 
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
@dataclass
class TPTPCompiler(Compiler):
    default_suffix: ClassVar[str] = "tptp"

    def compile(self, theory: Theory, syntax: Optional[Union[str, ModelSyntax]] = None, **kwargs) -> str:
        lines = [f"% Problem: {theory.name}"]
        grp_counts: Dict[str, int] = defaultdict(int)
        for sg in theory.sentence_groups:
            if sg.group_type == SentenceGroupType.GOAL:
                typ = "conjecture"
            else:
                typ = "axiom"
            for s in sg.sentences or []:
                t = as_tptp(s)
                grp_counts[typ] += 1
                lines.append(f"fof(axiom{grp_counts[typ]}, axiom, {t}).")
        return "\n".join(lines)