Sequents¶
Base Classes¶
-
class
logics.classes.propositional.proof_theories.
Sequent
(*args, **kwargs)¶ Class for representing sequents.
Extends
list
instead ofInference
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 inLanguage
).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
- 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
-
property
-
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
, orA | ... | 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 isfast_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 dictsreturn_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)