# 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)
```