Logic

class gavel.logic.logic.BinaryConnective

An enumeration.

class gavel.logic.logic.BinaryFormula(left: gavel.logic.logic.LogicElement, operator, right: gavel.logic.logic.LogicElement)

Variables:

• oparator – A binary operator
• left – The formula on the left side
• right – The formula on the right side

class gavel.logic.logic.DefinedConstant

An enumeration.

class gavel.logic.logic.DefinedPredicate

An enumeration.

class gavel.logic.logic.QuantifiedFormula(quantifier, variables, formula)

Variables:

• quantifier – A quantier (existential or universal)
• variables – A list of variables bound by the quantifier
• formula – A logical formula

class gavel.logic.logic.Quantifier

An enumeration.

class gavel.logic.logic.UnaryConnective

An enumeration.

class gavel.logic.logic.UnaryFormula(connective, formula: gavel.logic.logic.LogicElement)

Variables:

• connective – A unary connective
• formula – A formula

Problem

class gavel.logic.problem.FormulaRole

An enumeration.

class gavel.logic.problem.Problem(premises: Iterable[gavel.logic.problem.Sentence], conjecture: Iterable[gavel.logic.problem.Sentence], imports=None)

This class stores the important information that are needed for a proof

Variables:

• premises (gavel.logic.logic.Sentence) – The premises available for this problem
• conjecture (gavel.logic.logic.Sentence) – The conjecture that should be proven`

Proof

class gavel.logic.proof.Axiom(formula: gavel.logic.logic.LogicElement = None, name: str = None, **kwargs)

class gavel.logic.proof.Inference(antecedents: Iterable[gavel.logic.proof.ProofStep] = None, conclusion: gavel.logic.logic.LogicElement = None, **kwargs)

class gavel.logic.proof.Introduction(introduction_type: gavel.logic.proof.IntroductionType = None, **kwargs)

class gavel.logic.proof.IntroductionType

An enumeration.

class gavel.logic.proof.ProofStep(formula: gavel.logic.logic.LogicElement = None, name: str = None, **kwargs)