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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
@dataclass
class TPTPCompiler(Compiler):
    default_suffix: ClassVar[str] = "tptp"

    def compile(self, theory: Theory, syntax: Optional[Union[str, ModelSyntax]] = None, **kwargs) -> str:
        """
        A Compiler that generates TPTP code from a Theory object.

        Example:

            >>> from typedlogic import *
            >>> theory = Theory()
            >>> x = Variable("x")
            >>> theory.predicate_definitions = [PredicateDefinition("P", {"x": "str"}),
            ...              PredicateDefinition("Q", {"x": "str"})]
            >>> s = Implies(Term("P", x), Term("Q", x))
            >>> theory.add(sentence=s)
            >>> compiler = TPTPCompiler()
            >>> print(compiler.compile(theory))
            % Problem: None
            fof(axiom1, axiom, (p(X) => q(X))).

        :param theory:
        :param syntax:
        :param kwargs:
        :return:
        """
        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)

compile(theory, syntax=None, **kwargs)

A Compiler that generates TPTP code from a Theory object.

Example:

>>> from typedlogic import *
>>> theory = Theory()
>>> x = Variable("x")
>>> theory.predicate_definitions = [PredicateDefinition("P", {"x": "str"}),
...              PredicateDefinition("Q", {"x": "str"})]
>>> s = Implies(Term("P", x), Term("Q", x))
>>> theory.add(sentence=s)
>>> compiler = TPTPCompiler()
>>> print(compiler.compile(theory))
% Problem: None
fof(axiom1, axiom, (p(X) => q(X))).

Parameters:

Name Type Description Default
theory Theory
required
syntax Optional[Union[str, ModelSyntax]]
None
kwargs
{}

Returns:

Type Description
str
Source code in src/typedlogic/compilers/tptp_compiler.py 
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
def compile(self, theory: Theory, syntax: Optional[Union[str, ModelSyntax]] = None, **kwargs) -> str:
    """
    A Compiler that generates TPTP code from a Theory object.

    Example:

        >>> from typedlogic import *
        >>> theory = Theory()
        >>> x = Variable("x")
        >>> theory.predicate_definitions = [PredicateDefinition("P", {"x": "str"}),
        ...              PredicateDefinition("Q", {"x": "str"})]
        >>> s = Implies(Term("P", x), Term("Q", x))
        >>> theory.add(sentence=s)
        >>> compiler = TPTPCompiler()
        >>> print(compiler.compile(theory))
        % Problem: None
        fof(axiom1, axiom, (p(X) => q(X))).

    :param theory:
    :param syntax:
    :param kwargs:
    :return:
    """
    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)