Dialects

Parser

Gavel comes with a collection of parsers for different logical frameworks. You can use these parsers to parse a single expression from a string:

from gavel.dialects.tptp.parser import TPTPParser

parser = TPTPParser()
string = "cnf(name, axiom, a | b)."

structure = parser.parse_single_from_string(string)
print(structure.formula)

(a) | (b)

In most cases the exact structrue of the input is not known, e.g. it might contain several expressions. To extract all lines from a string use the parse_single_from_string which returns a generator of found expressions

string = "cnf(name, axiom, a | b).cnf(name, axiom, d | e)."

for line in parser.stream_formula_lines(string):
    structure = parser.parse_single_from_string(line)
    print(structure.formula)

(a) | (b)
(d) | (e)

If you want to parse a complete problem from a file, use the specific problem parser. As some reasoners (e.g. SPASS) do not accept problems that cotain multiple conjectures, ProblemParser.parse returns a generator of problems, containing one conjecture each.

from gavel.dialects.tptp.parser import TPTPProblemParser

problem_parser = TPTPProblemParser()
string = "cnf(a1, axiom, a | b).cnf(a1, axiom, ~a).cnf(a2, negated_conjecture, b)."

for problem in problem_parser.parse(string):
    print("Axioms:")
    for a in problem.premises:
        print(a.formula)
    print("Conjecture:")
    print(problem.conjecture.formula)

Axioms:
(a) | (b)
~(a)
Conjecture:
b

class gavel.dialects.base.parser.LogicParser

class gavel.dialects.base.parser.Parser

parse(structure: Parseable, *args, **kwargs) → Target

Transforms the input structure into metadata as used by the OpenEnergyPlatform

Parameters:inp (str) – The input string that should be parsed into OEP metadata Returns:OEPMetadata – OEP metadata represented by inp

exception gavel.dialects.base.parser.ParserException

class gavel.dialects.base.parser.ProblemParser(*args, **kwargs)

logic_parser_cls

alias of LogicParser

parse(inp, *args, **kwargs)

Transforms the input structure into metadata as used by the OpenEnergyPlatform

Parameters:inp (str) – The input string that should be parsed into OEP metadata Returns:OEPMetadata – OEP metadata represented by inp

class gavel.dialects.base.parser.ProofParser

class gavel.dialects.base.parser.StringBasedParser

static _unpack_file(*args, **kwargs) → Iterable[str]

is_valid(inp: str) → bool

Verify if inp is a sting representation that is parsable by this parser :Parameters: inp (str) – String to verify

Returns:bool – Indicated whether this object is parsable or not

load_single_from_string(string: str, *args, **kwargs) → Parseable

Load a string into the structure represented by the dialect

Parameters:string

parse_single_from_string(string: str, load_args=None, parse_args=None, load_kwargs=None, parse_kwargs=None) → Target

Parse a string into OEPMetadata

Parameters:string

Compiler