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:

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:
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:

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:

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:

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:
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)