Sequents¶

Base Classes¶

class logics.classes.propositional.proof_theories.Sequent(*args, **kwargs)¶

Class for representing sequents.

Extends list instead of Inference because that allows us to have n-sided calculi. Standard 2-sided sequents will be len2-lists, 3-sided will be len3-lists, etc. Also, unlike Inferences, there are no nested Sequents (Sequents inside other Sequents). All are level 1.

Context variables are represented as strings, not Formula (see the parameter in Language).

Also notice that, since sequents are lists of lists, order and repetition of formulae within sides matter, e.g. Γ, A ⇒ B, Δ is not the same as Γ, A ⇒ Δ, B nor of Γ, Γ, A ⇒ B, B, Δ.

Examples

>>> from logics.classes.propositional import Formula
>>> from logics.classes.propositional.proof_theories import Sequent
>>> seq1 = Sequent([['Γ', Formula(['A'])], [Formula(['B']), 'Δ']])  # A 2-sided sequent
>>> seq1
[['Γ', ['A']], [['B'], 'Δ']]
>>> seq2 = Sequent([['Γ', Formula(['A'])], [Formula(['B']), 'Δ'], [Formula(['C']), 'Σ']])  # A 3-sided sequent
>>> seq2
[['Γ', ['A']], [['B'], 'Δ'], [['C'], 'Σ']]

As said above, order and repetition matter:

>>> seq3 = Sequent([[Formula(['A']), 'Γ'], [Formula(['B']), 'Δ']])
>>> seq3 == seq1
False

You can also use parsers to get sequents:

>>> from logics.utils.parsers import classical_parser
>>> seq4 = classical_parser.parse("Gamma, A ==> B, Delta")
>>> seq4
[['Γ', ['A']], [['B'], 'Δ']]
>>> seq4 == seq1
True
>>> seq5 = classical_parser.parse("Gamma, A | B, Delta | C, Sigma")
[['Γ', ['A']], [['B'], 'Δ'], [['C'], 'Σ']]
>>> seq5 == seq2
True

The parser can also be used for unparsing (pretty printing) sequents:

>>> classical_parser.unparse(seq1)
'Γ, A ⇒ B, Δ'
>>> classical_parser.unparse(seq2)
'Γ, A | B, Δ | C, Σ'

property sides¶

Property that returns the number of sides.

Examples

>>> from logics.utils.parsers import classical_parser
>>> seq1 = classical_parser.parse("Gamma, A ==> B, Delta")
>>> seq1.sides
2
>>> seq2 = classical_parser.parse("Gamma, A | B, Delta | C, Sigma")
>>> seq2.sides
3

property antecedent¶

Returns the antecedent (first side) for 2-sided sequents, a ValueError for n>2-sided sequents.

Examples

>>> from logics.utils.parsers import classical_parser
>>> seq1 = classical_parser.parse("Gamma, A ==> B, Delta")
>>> seq1.antecedent
['Γ', ['A']]
>>> seq2 = classical_parser.parse("Gamma, A | B, Delta | C, Sigma")
>>> seq2.antecedent
Traceback (most recent call last):
...
ValueError: n>2-sided sequents do not have antecedent and succedent

property succedent¶

Same as above but with the succedent. Only works for 2-sided sequents.

Examples

>>> from logics.utils.parsers import classical_parser
>>> seq1 = classical_parser.parse("Gamma, A ==> B, Delta")
>>> seq1.succedent
[['B'], 'Δ']
>>> seq2 = classical_parser.parse("Gamma, A | B, Delta | C, Sigma")
>>> seq2.succedent
Traceback (most recent call last):
...
ValueError: n>2-sided sequents do not have antecedent and succedent

main_formulae(language)¶

Given a language, will return all the non-context formulae in a sequent (with repetitions).

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.languages import classical_language
>>> seq1 = classical_parser.parse("Gamma, A ==> A, B, Delta")
>>> seq1.main_formulae(classical_language)
[['A'], ['A'], ['B']]

context_formulae(language)¶

Same as above but with the context formulae.

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.languages import classical_language
>>> seq1 = classical_parser.parse("Gamma, A ==> Gamma, B, Delta")
>>> seq1.context_formulae(classical_language)
['Γ', 'Γ', 'Δ']

substitute(language, sf_to_substitute, sf_with)¶

Substitute stuff within sequents.

Parameters

language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
sf_to_substitute (logics.classes.propositional.Formula or str or list of the previous) – Can substitute either a formula, a context variable or an entire slice of a sequent
sf_with (logics.classes.propositional.Formula or str or list of the previous) – Can substitute it with either a formula, a context variable or an entire slice of a sequent

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.languages import classical_language
>>> seq = classical_parser.parse("Γ, ~~A ==> ~A, Δ")

Substitute a (sub)formula for another formula, or a formula for a context variable:

>>> subst1 = seq.substitute(classical_language, classical_parser.parse("~A"), classical_parser.parse("D"))
>>> classical_parser.unparse(subst1)
'Γ, ~D ⇒ D, Δ'
>>> subst2 = seq.substitute(classical_language, classical_parser.parse("~~A"), "Δ")
>>> classical_parser.unparse(subst2)
'Γ, Δ ⇒ ~A, Δ'

Substitute a context variable for either a formula or another context variable:

>>> subst3 = seq.substitute(classical_language, "Γ", classical_parser.parse("D"))
>>> classical_parser.unparse(subst3)
'D, ~~A ⇒ ~A, Δ'
>>> subst4 = seq.substitute(classical_language, "Γ", "Δ")
>>> classical_parser.unparse(subst4)
'Δ, ~~A ⇒ ~A, Δ'

Substitute a formula or a context variable for a slice (list):

>>> subst5 = seq.substitute(classical_language, classical_parser.parse("~~A"), ["Δ", classical_parser.parse("D")])
>>> classical_parser.unparse(subst5)
'Γ, Δ, D ⇒ ~A, Δ'
>>> subst6 = seq.substitute(classical_language, "Γ", ["Δ", classical_parser.parse("D")])
>>> classical_parser.unparse(subst6)
'Δ, D, ~~A ⇒ ~A, Δ'

Substitute a slice (list) for either a formula or a context variable:

>>> subst7 = seq.substitute(classical_language, ["Γ", classical_parser.parse("~~A")], "Δ")
>>> classical_parser.unparse(subst7)
'Δ ⇒ ~A, Δ'

Substitute a slice (list) for another slice:

>>> subst8 = seq.substitute(classical_language, ["Γ", classical_parser.parse("~~A")], ["Δ", classical_parser.parse("D")])
>>> classical_parser.unparse(subst8)
'Δ, D ⇒ ~A, Δ'

Through all this, the original sequent remains unaltered:

>>> classical_parser.unparse(seq)
'Γ, ~~A ⇒ ~A, Δ'

side_substitute(side, language, sf_to_substitute, sf_with)¶

Same as above but takes a sequent side (a list) rather than an entire Sequent

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.languages import classical_language
>>> seq = classical_parser.parse("Γ, ~~A ==> ~A, Δ")
>>> seq.side_substitute(seq.antecedent, classical_language, classical_parser.parse("~A"), classical_parser.parse("D"))
['Γ', ['~', ['D']]]

instantiate(language, subst_dict)¶

Given a language and a substitution dict, returns the Sequent instantiated with the dict.

Will return a different Sequent object, and not modify the original. For instantiating formulae, the susbstitution dict must have form {'A': someformula, 'B': someformula}. Context variables can represent multiple formulae, so they must be instantiated with lists, e.g. {'Γ': ['Σ', Formula(['A'])], 'Δ': ['Δ']}

Parameters

language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
subst_dict (dict) – See above for the format

Returns

A different sequent instance from the original

Return type

logics.classes.propositional.proof_theories.Sequent

Raises

ValueError – if some schematic propositional or context variable within the formula has no substitution assigned in the dictionary

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.languages import classical_language
>>> sequent1 = classical_parser.parse('Γ, A, Δ, ~p ==>')
>>> B = classical_parser.parse("B")
>>> inst1 = sequent1.instantiate(classical_language, {'A': B, 'Γ': ['Δ', B], 'Δ': ['Δ']})
>>> classical_parser.unparse(inst1)
'Δ, B, B, Δ, ~p ⇒ '
>>> classical_parser.unparse(sequent1)  # sequent1 is unmodified
'Γ, A, Δ, ~p ⇒ '
>>> sequent1.instantiate(classical_language, {'A': B, 'Γ': ['Δ', B]})
Traceback (most recent call last):
...
ValueError: Context variable Δ not present in substitution dict

is_instance_of(rule_sequent, language, possible_subst_dicts=None, return_subst_dicts=False)¶

Determines if a sequent is an instance of another sequent (which is tipically within a rule).

Works similarly to Formula.is_instance_of() but has one big difference: A sequent can be an instance of another sequent in many possible ways (i.e. with many possible substitution dicts). For example, Γ, A, B, Δ ⇒ is an instance of Γ, A, Δ ⇒; but unlike with formulae, it is not univocally determined which formula/context variable in the second corresponds to which in the first. It could be the case that {Γ: [Γ], A: A, Δ: [B, Δ]} or that {Γ: [Γ, A], A: B, Δ: Δ}. This is also very important in determining if an application of a rule is correct (see the source code comment for some examples).

Thus, the two optional parameters are a bit different:

possible_subst_dicts: defaults to None. Is a list of all the possible substitution dicts. If given, at least one of them should be the case.

return_subst_dicts: defaults to False. If True, will return the list of all possible substitution dicts (i.e. a list of dicts)

Parameters

rule_sequent (logics.classes.propositional.proof_theories.Sequent) – The Sequent of which we want to know if it is instance
language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
possible_subst_dicts (dict, optional) – A list of susbstitution dicts of the form {'A': someformula, 'Γ': [...]}
return_subst_dicts (bool, optional) – If True will additionally return a list of possible substitution dicts

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.languages import classical_language
>>> sequent1 = classical_parser.parse("Γ, A, Δ ⇒")
>>> sequent2 = classical_parser.parse("Γ, A, B, Δ ⇒")
>>> sequent2.is_instance_of(sequent1, classical_language)
True
>>> sequent2.is_instance_of(sequent1, classical_language, return_subst_dicts=True)
(True, [{'A': ['A'], 'Γ': ['Γ'], 'Δ': [['B'], 'Δ']}, {'A': ['B'], 'Γ': ['Γ', ['A']], 'Δ': ['Δ']}])
>>> sequent2.is_instance_of(sequent1, classical_language,
...                         possible_subst_dicts=[{'A': ['B'], 'Γ': ['Γ', ['A']], 'Δ': ['Δ']}])
True
>>> sequent2.is_instance_of(sequent1, classical_language,
...                         possible_subst_dicts=[{'A': ['B'], 'Γ': ['Γ', ['A']], 'Δ':[['B'], 'Δ']}])
False

class logics.classes.propositional.proof_theories.SequentNode(content, justification=None, parent=None, children=None)¶

Class for nodes in sequent tree-derivations.

Subclasses NodeMixin from the anytree package. Since a node can have children, it can also be taken to represent a tree (an entire derivation), see below for some examples.

Unlike tableaux nodes, these must be read backwards: The parent sequent is the derived sequent and the children are its premises.

Parameters

content (logics.classes.propositional.proof_theories.Sequent) – The sequent of the node
justification (str, optional) – If the node is non-root, this parameter should contain the name of the rule by which it was obtained
parent (logics.classes.propositional.proof_theories.SequentNode, optional) – The parent node. The root node of a tableaux has None as parent (the default value).
children (list of logics.classes.propositional.proof_theories.SequentNode, optional) – A list of the children node. Also optional. If child nodes are specified with the parent attribute, there is no need to provide this (see the example below).

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import SequentNode
>>> n3 = SequentNode(content=classical_parser.parse('A, Gamma ==> Delta'))
>>> n2 = SequentNode(content=classical_parser.parse('Gamma ==> Delta, ~A'), justification='~R', children=[n3])
>>> n1 = SequentNode(content=classical_parser.parse('Gamma ==> ~A, Delta'), justification='ER', children=[n2])

As in tableaux, we can pretty print like this:

>>> n1.print_tree(classical_parser)
Γ ⇒ ~A, Δ (ER)
└── Γ ⇒ Δ, ~A (~R)
    └── A, Γ ⇒ Δ

Also as in tableaux nodes, the anytree package gives us some base functionality:

>>> n1.is_root
True
>>> n3.is_leaf
True
>>> n1.children  # returns (n2,)
([['Γ'], ['Δ', ['~', ['A']]]] (~R),)
>>> n1.descendants  # returns (n2, n3)
([['Γ'], ['Δ', ['~', ['A']]]] (~R), [[['A'], 'Γ'], ['Δ']])
>>> n3.root  # returns n1
[['Γ'], [['~', ['A']], 'Δ']] (ER)
>>> n1.leaves  # returns (n3,)
([[['A'], 'Γ'], ['Δ']],)
>>> n3.path  # returns (n1, n2, n3)
([['Γ'], [['~', ['A']], 'Δ']] (ER), [['Γ'], ['Δ', ['~', ['A']]]] (~R), [[['A'], 'Γ'], ['Δ']])
>>> n3.depth
2
>>> n1.height
2

is_instance_of(node, language, possible_subst_dicts=None, return_subst_dicts=False)¶

Determines if a SequentNode is an instance of another SequentNode

A node is considered an instance of another iff:

The content of self is an instance of the content of node
The justification is equal to the justification of node (or is None in node)

return_subst_dicts and possible_subst_dicts are as in Sequent.is_instance_of (and are used for uniform substitution).

Parameters

node (logics.classes.propositional.proof_theories.SequentNode) – The SequentNode of which we want to know if it is instance
language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
possible_subst_dicts (dict, optional) – A list of susbstitution dicts of the form {'A': someformula, 'Γ': [...]}
return_subst_dicts (bool, optional) – If True will additionally return a list of possible substitution dicts.

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.languages import classical_language
>>> from logics.classes.propositional.proof_theories import SequentNode
>>> n1 = SequentNode(content=classical_parser.parse('Gamma, ~A, Delta ==>'))
>>> n2 = SequentNode(content=classical_parser.parse('Gamma, ~p, ~~p ==>'))
>>> n2.is_instance_of(n1, classical_language)
True
>>> n2.is_instance_of(n1, classical_language, return_subst_dicts=True)
(True, [{'A': ['p'], 'Γ': ['Γ'], 'Δ': [['~', ['~', ['p']]]]}, {'A': ['~', ['p']], 'Γ': ['Γ', ['~', ['p']]], 'Δ': []}])
>>> n3 = SequentNode(content=classical_parser.parse('Gamma, ~p, ~~p ==>'), justification='~L')
>>> n3.is_instance_of(n1, classical_language)  # justification is None in n1
True
>>> n4 = SequentNode(content=classical_parser.parse('Gamma, ~A, Delta ==>'), justification='~L')
>>> n2.is_instance_of(n4, classical_language)  # Justification is None in n2 but not in n4
False

print_tree(parser=None)¶

Will print a node and its descendants in a pretty, tree-like, format

If a parser is given as argument, returns the content unparsed. See above for an example.

Sequent Calculus¶

class logics.classes.propositional.proof_theories.SequentCalculus(language, axioms, rules, solver=None, solver_rule_order=None)¶

Class for sequent calculi systems

Parameters

language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
axioms (dict (str: logics.classes.propositional.proof_theories.Sequent)) – The keys are strings (the name of the rule) and the values are Sequent
rules (dict (str: logics.classes.propositional.proof_theories.SequentNode)) – The keys are strings (the name of the rule) and the values are SequentNode (w/children)
solver – Any object with a reduce method (which takes a sequent and a sequent calculus). None by default.
solver_rule_order (list of str) – The order of rules (given as rule names) in which the solver should try to reduce a sequent. If smart_weakening is activated in the solver (see the solver class) the weakening rules can be obviated here.

fast_axiom_check¶

Class attribute. If true, will assume that the only axiom present is identity without context (i.e. A ⇒ A, or A | ... | A). It is less general but the reducer works faster with this enabled. True by default.

Type: bool

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.languages import classical_language
>>> from logics.classes.propositional.proof_theories import Sequent, SequentNode, SequentCalculus

Defining some axioms and rules:

>>> identity = classical_parser.parse('A ==> A')
>>> weakening_left_premise = SequentNode(content=classical_parser.parse('Gamma ==> Delta'))
>>> weakening_left = SequentNode(content=classical_parser.parse('A, Gamma ==> Delta'),
...                              children=[weakening_left_premise])
>>> weakening_left.print_tree(classical_parser)  # For illustration purposes
A, Γ ⇒ Δ
└── Γ ⇒ Δ
>>> weakening_right_premise = SequentNode(content=classical_parser.parse('Gamma ==> Delta'))
>>> weakening_right = SequentNode(content=classical_parser.parse('Gamma ==> Delta, A'),
...                               children=[weakening_right_premise])
>>> weakening_right.print_tree(classical_parser)  # For illustration purposes
Γ ⇒ Δ, A
└── Γ ⇒ Δ
>>> negation_left_premise = SequentNode(content=classical_parser.parse('Gamma ==> Delta, A'))
>>> negation_left = SequentNode(content=classical_parser.parse('~A, Gamma ==> Delta'),
...                             children=[negation_left_premise])
>>> negation_left.print_tree(classical_parser)  # For illustration purposes
~A, Γ ⇒ Δ
└── Γ ⇒ Δ, A
>>> negation_right_premise = SequentNode(content=classical_parser.parse('A, Gamma ==> Delta'))
>>> negation_right = SequentNode(content=classical_parser.parse('Gamma ==> Delta, ~A'),
...                              children=[negation_right_premise])
>>> negation_right.print_tree(classical_parser)  # For illustration purposes
Γ ⇒ Δ, ~A
└── A, Γ ⇒ Δ

Defining an example (toy) system with only weakening and negation rules:

>>> toy_system = SequentCalculus(language=classical_language, axioms={'identity': identity},
...                              rules={'WL': weakening_left, 'WR': weakening_right,
...                                     '~L': negation_left, '~R': negation_right})

sequent_is_axiom(sequent, axiom_name=None)¶

Determines if a sequent is an instance of an axiom of the system.

Parameters

sequent (logics.classes.propositional.proof_theories.Sequent) – The sequent you wish to check
axiom_name (str, optional) – If left as None will check every axiom of the system. If given a string (an axiom name) will only check that particular axiom. Giving a string will do nothing is fast_axiom_check is enabled.

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.sequents import LK
>>> seq = classical_parser.parse("p ==> p")
>>> LK.sequent_is_axiom(seq)
True
>>> seq2 = classical_parser.parse("p, Gamma ==> Delta, p")
>>> LK.sequent_is_axiom(seq2)
False

tree_is_closed(node)¶

Given a tree (a derived sequent with children -premises-) checks if all descendant branches are closed (i.e. if every leaf is an axiom)

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import SequentNode
>>> from logics.instances.propositional.sequents import LK
>>> n1 = SequentNode(content=classical_parser.parse('A ==> A'), justification='identity')
>>> n2 = SequentNode(content=classical_parser.parse('A ==> A, Delta'), justification='WR', children=[n1])
>>> n3 = SequentNode(content=classical_parser.parse('Gamma, A ==> A, Delta'), justification='WL', children=[n2])
>>> n3.print_tree(classical_parser)  # for illustration purposes
Γ, A ⇒ A, Δ (WL)
└── A ⇒ A, Δ (WR)
    └── A ⇒ A (identity)
>>> LK.tree_is_closed(n3)
True
>>> n2.children = []
>>> LK.tree_is_closed(n2)
False

is_correctly_applied(node, rule_name, return_subst_dicts=False, return_error=False)¶

Checks if a node and its immediate descentants are an instance of a given rule

Parameters

node (logics.classes.propositional.proof_theories.SequentNode) – A sequent node (derived) w/children (premises)
rule_name (str) – The name of the rule you want to check
return_subst_dicts (bool, optional) – If set to True will return a list of the possible substitution dicts
return_error (bool, optional) – If True will return a string detailing the error it found (just one, not a list of errors)

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import SequentNode
>>> from logics.instances.propositional.sequents import LK
>>> n1 = SequentNode(content=classical_parser.parse('A ==> A'), justification='identity')
>>> n2 = SequentNode(content=classical_parser.parse('A ==> A, Delta'), justification='WR', children=[n1])
>>> n2.print_tree(classical_parser)  # for illustration purposes
A ⇒ A, Δ (WR)
└── A ⇒ A (identity)
>>> LK.is_correctly_applied(n2, "WR")
True
>>> LK.is_correctly_applied(n2, "WR", return_subst_dicts=True)  # (weakening is defined with context vars)
(True, [{'Γ': [['A']], 'Δ': [['A']], 'Π': ['Δ']}])
>>> n2.justification = "WL"
>>> LK.is_correctly_applied(n2, "WL")
False
>>> LK.is_correctly_applied(n2, "WL", return_error=True)
(False, "... premise [[['A']], [['A']]] (identity) is not an instance of rule premise [['Γ'], ['Δ']]")

is_correct_tree(tree, premises=None, return_error_list=False, exit_on_first_error=False)¶

Checks if a tree derivation is correct.

That is, checks that every leaf is an axiom or a premise, and that every other node is obtained via a correct application of a rule to its children nodes. Remember that the root of the tree is the derived node.

Parameters

tree (logics.classes.propositional.proof_theories.SequentNode) – A sequent tree (derivation)
premises (list of logics.classes.propositional.proof_theories.Sequent, optional) – An optional list of sequents to use as premises, additionally to the axioms
return_error_list (bool, optional) – If False, will just return True or False (exits when it finds an error, more efficient) If True, will return (True, a list of logics.classes.errors.CorrectionError)
exit_on_first_error (bool, optional) – If return_error_list and this are both true, it will return a list with a single error instead of many. More efficient, since it makes early exits.

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.classes.propositional.proof_theories import SequentNode
>>> from logics.instances.propositional.sequents import LK

A correct derivation:

>>> n1 = SequentNode(content=classical_parser.parse('A ==> A'), justification='identity')
>>> n2 = SequentNode(content=classical_parser.parse('A ==> A, Delta'), justification='WR', children=[n1])
>>> n3 = SequentNode(content=classical_parser.parse('Gamma, A ==> A, Delta'), justification='WL', children=[n2])
>>> n3.print_tree(classical_parser)  # for illustration purposes
Γ, A ⇒ A, Δ (WL)
└── A ⇒ A, Δ (WR)
    └── A ⇒ A (identity)
>>> LK.is_correct_tree(n3)
True

An incorrect derivation (correct with premises):

>>> n4 = SequentNode(content=classical_parser.parse('p ==> q'))
>>> n5 = SequentNode(content=classical_parser.parse('p ==> q, Delta'), justification='WR', children=[n4])
>>> n6 = SequentNode(content=classical_parser.parse('Gamma, p ==> q, Delta'), justification='WL', children=[n5])
>>> n6.print_tree(classical_parser)  # for illustration purposes
Γ, p ⇒ q, Δ (WL)
└── p ⇒ q, Δ (WR)
    └── p ⇒ q
>>> LK.is_correct_tree(n6)
False
>>> LK.is_correct_tree(n6, return_error_list=True)
(False, [Node [[['p']], [['q']]]: Axiom None is not a valid axiom name, Node [[['p']], [['q']]] is not a valid axiom])
>>> LK.is_correct_tree(n6, premises=[classical_parser.parse('p ==> q')])
True

static transform_inference_into_sequent(inference, sides=2, separate_premises_from_conclusions_at_index=1)¶

Transforms an Inference into an n-sided sequent, in order to check for validity using sequent calculi.

Parameters

inference (logics.classes.propositional.Inference) – The inference you want to transform
sides (int, optional) – Number of sides you want the resulting sequent to have. Defaults to 2
separate_premises_from_conclusions_at_index (int, optional) – For n-sided calculi, where you want to separate the premises and conclusions. Defaults to 1

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.sequents import LK
>>> inf = classical_parser.parse("p ∨ q, ~p / q")
>>> seq = LK.transform_inference_into_sequent(inf)
>>> classical_parser.unparse(seq)
'(p ∨ q), ~p ⇒ q'
>>> seq = LK.transform_inference_into_sequent(inf, sides=3)
>>> classical_parser.unparse(seq)
'(p ∨ q), ~p | q | q'
>>> seq = LK.transform_inference_into_sequent(inf, sides=3, separate_premises_from_conclusions_at_index=2)
>>> classical_parser.unparse(seq)
'(p ∨ q), ~p | (p ∨ q), ~p | q'

reduce(sequent, premises=None)¶: Shortcut for solver.reduce(sequent, self, premises), see the solver documentation

is_valid(inference, sides=2, separate_premises_from_conclusions_at_index=1)¶

Determines if an Inference is valid.

Will only work if a solver was given to the init method when initializing the class. Default arguments assume a 2-sided calculus

Parameters

inference (logics.classes.propositional.Inference) – The inference you want to transform
sides (int, optional) – Number of sides you want the resulting sequent to have. Defaults to 2
separate_premises_from_conclusions_at_index (int, optional) – For n-sided calculi, where you want to separate the premises and conclusions. Defaults to 1

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.sequents import LKminEA  # see below in Instances for a description
>>> inf = classical_parser.parse("p ∨ q, ~p / q")
>>> LKminEA.is_valid(inf)
True
>>> inf2 = classical_parser.parse("p ∨ q / p")
>>> LKminEA.is_valid(inf2)
False

Instances¶

logics.instances.propositional.sequents.LK¶: The standard LK system with Cut. The structural rules are presented with context variables. E.g. WL is:

weakening_left_premise = SequentNode(content=classical_parser.parse('Gamma ==> Delta'))
weakening_left = SequentNode(content=classical_parser.parse('Pi, Gamma ==> Delta'),
                             children=[weakening_left_premise])

This is for the solver to be able to weaken context variables in LKmin (see below). Since LK has Cut, does have a solver (reducer) assigned. For the full list of rules, see the source code.

logics.instances.propositional.sequents.LKmin¶: Same as the above but with no Cut rule. Has a solver (which works extremely slowly).

logics.instances.propositional.sequents.LKminEA¶: A version of LKmin that works with sequences, like everything here, but has Exchange admissible (internalized into the other rules). Also uses a combination of additive and multiplicative rules. All this makes it much faster to work with for the solver.

Sequent Reducer¶

class logics.utils.solvers.sequents.SequentReducer(max_apparitions_per_side=None, smart_weakening=True, weakening_rule_names=None)¶

Solver for sequent calculi

Parameters

max_apparitions_per_side (int or None, optional) – In case you want to limit the number of apparitions of a formula in a side, set it to an int. Otherwise, leave it as None (default). Useful for when you have contraction as a solver rule and want n-reduced sequents (see Paoli, Substructural Logics: A Primer)
smart_weakening (bool, optional) – If True (default value), at every step of the reduction, will look for a formula present in all sides. If it finds it, starts from there and weakens its way into the current sequent to reduce. Makes the reducer faster in some contexts.
weakening_rule_names (dict {int: str}) – If smart_weakening is activated, you need to tell it the name of the rule to use in each side when appliying weakening. For example, weakening_rule_names = {0: 'WL', 1: 'WR'} (the key should be the index of the side)

reduce(sequent, sequent_calculus, premises=None, max_depth=100)¶

Reduces a sequent using the rules of the system given, and returns a tree (a SequentNode with children).

Will return the first reduction tree of a sequent that it finds, but there may be more. If it does not find any, will raise SolverError.

Parameters

sequent (logics.classes.propositional.proof_theories.Sequent) – The sequent to reduce
sequent_calculus (logics.classes.propositional.proof_theories.SequentCalculus) – The sequent calculus from which the rules are used
premises (list of logics.classes.propositional.proof_theories.Sequent, optional) – An optional list of sequents to use as premises, additionally to the axioms
max_depth (int, optional) – The maximum depth that a tree can have. If it hits it, exits with a SolverError. Defaults to 100

Raises

logics.classes.exceptions.SolverError – If it cannot find a reduction for the given sequent or hits the max_depth limit

Examples

>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.sequents import LKminEA
>>> from logics.utils.solvers.sequents import LKminEA_sequent_reducer
>>> seq = classical_parser.parse('Gamma ==> Delta, (A or not A)')
>>> tree= LKminEA_sequent_reducer.reduce(seq, LKminEA)
>>> tree.print_tree(classical_parser)
Γ ⇒ Δ, (A ∨ ~A) (∨R1)
└── Γ ⇒ Δ, A, ~A (~R)
    └── Γ, A ⇒ Δ, A (WR)
        └── Γ, A ⇒ A (WL)
            └── A ⇒ A (identity)
>>> seq2 = classical_parser.parse('Gamma ==> Delta, (A and not A)')
>>> LKminEA_sequent_reducer.reduce(seq2, LKminEA)
Traceback (most recent call last):
...
logics.classes.exceptions.SolverError: Could not find reduction for [['Γ'], ['Δ', ['∧', ['A'], ['~', ['A']]]]]
>>> seq3 = classical_parser.parse('A, ~B ==>')
>>> tree3 = LKminEA_sequent_reducer.reduce(seq3, LKminEA, premises=[classical_parser.parse("A ==> B")])
>>> tree3.print_tree(classical_parser)
A, ~B ⇒  (~L)
└── A ⇒ B (premise)