Skip to content

FOR Compiler

Bases: Compiler

A compiler that generates First Order Logic (FOL) syntax.

Source code in src/typedlogic/compilers/fol_compiler.py 
 9
10
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
@dataclass
class FOLCompiler(Compiler):
    """
    A compiler that generates First Order Logic (FOL) syntax.
    """

    default_suffix: ClassVar[str] = "fol"

    def compile(self, theory: Theory, syntax: Optional[Union[str, ModelSyntax]] = None, **kwargs) -> str:
        """
        Compile a Theory object into FOL syntax.

        Example:
        -------
            >>> from typedlogic.registry import get_compiler
            >>> from typedlogic import *
            >>> theory = Theory()
            >>> x = Variable("x")
            >>> theory.predicate_definitions = [PredicateDefinition("P", {"x": "str"}),
            ...              PredicateDefinition("Q", {"x": "str"})]
            >>> s = Forall([x], Implies(Term("P", x), Term("Q", x)))
            >>> theory.add(sentence=s)
            >>> compiler = get_compiler("fol")
            >>> print(compiler.compile(theory))
            ∀[x]. P(x) → Q(x)

        :param theory:
        :param syntax:
        :param kwargs:
        :return:

        """
        lines = []
        for s in theory.sentences:
            lines.append(as_fol(s))
        return "\n".join(lines)

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

Compile a Theory object into FOL syntax.

Example:

>>> from typedlogic.registry import get_compiler
>>> from typedlogic import *
>>> theory = Theory()
>>> x = Variable("x")
>>> theory.predicate_definitions = [PredicateDefinition("P", {"x": "str"}),
...              PredicateDefinition("Q", {"x": "str"})]
>>> s = Forall([x], Implies(Term("P", x), Term("Q", x)))
>>> theory.add(sentence=s)
>>> compiler = get_compiler("fol")
>>> print(compiler.compile(theory))
∀[x]. 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/fol_compiler.py 
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
def compile(self, theory: Theory, syntax: Optional[Union[str, ModelSyntax]] = None, **kwargs) -> str:
    """
    Compile a Theory object into FOL syntax.

    Example:
    -------
        >>> from typedlogic.registry import get_compiler
        >>> from typedlogic import *
        >>> theory = Theory()
        >>> x = Variable("x")
        >>> theory.predicate_definitions = [PredicateDefinition("P", {"x": "str"}),
        ...              PredicateDefinition("Q", {"x": "str"})]
        >>> s = Forall([x], Implies(Term("P", x), Term("Q", x)))
        >>> theory.add(sentence=s)
        >>> compiler = get_compiler("fol")
        >>> print(compiler.compile(theory))
        ∀[x]. P(x) → Q(x)

    :param theory:
    :param syntax:
    :param kwargs:
    :return:

    """
    lines = []
    for s in theory.sentences:
        lines.append(as_fol(s))
    return "\n".join(lines)