Logics is a Python framework for mathematical logic
Project description
Logics is a Python framework for mathematical logic. It aims at generality (being able to represent as many systems as possible), well-documented and readable code and minimal dependencies, rather than speed. Some of its intended applications are educational software (e.g. TAUT, which uses a previous version of this package), and quick prototyping of ideas for research purposes.
To see the documentation, visit this link.
Installation
To install using pip:
$ pip install logics
Or clone it from this repository:
$ git clone https://github.com/ariroffe/logics.git
Examples
The following are some random examples of what you can do with this package. For a full specification of the functionality see the documentation.
Define a language:
>>> from logics.classes.propositional import Language >>> language = Language(atomics=['p', 'q', 'r'], ... constant_arity_dict={'~': 1, '∧': 2}, ... sentential_constants=['⊥', '⊤'], ... metavariables=['A', 'B', 'C'], ... context_variables=['Γ', 'Δ', 'Σ', 'Λ', 'Π', 'Θ'])
Construct formulae and inferences/metainferences, and use specific methods of those classes:
>>> from logics.utils.parsers import classical_parser >>> formula = classical_parser.parse('~(p and not q)') >>> inference = classical_parser.parse('(p / p) // (q / p & not p)') >>> type(formula) <class 'logics.classes.propositional.formula.Formula'> >>> type(inference) <class 'logics.classes.propositional.inference.Inference'> >>> formula.depth 3 >>> formula.is_well_formed(language) True >>> formula.is_instance_of(classical_parser.parse('not (A and B)'), language) True >>> formula2 = formula.substitute(classical_parser.parse("p"), classical_parser.parse("p or q")) >>> classical_parser.unparse(formula2) '~((p ∨ q) ∧ ~q)' >>> inference.level 2
Define a mixed many-valued model theory, and use it:
>>> from logics.instances.propositional.languages import classical_infinite_language_with_sent_constants >>> from logics.classes.propositional.semantics import MixedManyValuedSemantics >>> trivalued_truth_values = ['1', 'i', '0'] >>> trivalued_truth_functions = { ... '~': ['0', 'i', '1'], ... '∧': [ #1 #i #0 ... ['1', 'i', '0'], # 1 ... ['i', 'i', '0'], # i ... ['0', '0', '0']], # 0 ... '∨': [ #1 #i #0 ... ['1', '1', '1'], # 1 ... ['1', 'i', 'i'], # i ... ['1', 'i', '0']], # 0 ... '→': [ #1 #i #0 ... ['1', 'i', '0'], # 1 ... ['1', 'i', 'i'], # i ... ['1', '1', '1']], # 0 ... '↔': [ #1 #i #0 ... ['1', 'i', '0'], # 1 ... ['i', 'i', 'i'], # i ... ['0', 'i', '1']], # 0 ... } >>> ST = MixedManyValuedSemantics(language=classical_infinite_language_with_sent_constants, ... truth_values=trivalued_truth_values, ... premise_designated_values=['1'], ... conclusion_designated_values=['1', 'i'], ... truth_function_dict=trivalued_truth_functions, ... sentential_constant_values_dict={'⊥': '0', '⊤': '1'}, ... name='ST') >>> ST.valuation(classical_parser.parse('p then q'), {'p': '1', 'q': 'i'}) 'i' >>> ST.satisfies(classical_parser.parse('(A / B), (B / C) // (A / C)'), {'A': '1', 'B': 'i', 'C': '0'}) False >>> ST.is_valid(classical_parser.parse('p and ~p / q')) True >>> ST.is_locally_valid(classical_parser.parse('(A / B), (B / C) // (A / C)')) False >>> ST.is_globally_valid(classical_parser.parse('(A / B), (B / C) // (A / C)')) True >>> # There are also some predefined systems (ST is one of them, the above was unnecesary) >>> from logics.instances.propositional.many_valued_semantics import TS_mvl_semantics as TS >>> from logics.instances.propositional.many_valued_semantics import LP_mvl_semantics as LP >>> LP.is_valid(classical_parser.parse('p and ~p / q')) False >>> from logics.classes.propositional.semantics import MixedMetainferentialSemantics >>> TSST = MixedMetainferentialSemantics([TS, ST]) >>> TSST.is_locally_valid(classical_parser.parse('(A / B), (B / C) // (A / C)')) True
As in TAUT, logics has natural deduction module:
>>> # You can define your own natural deduction system, here we will just import a predefined instance: >>> from logics.instances.propositional.natural_deduction import classical_natural_deduction_system >>> from logics.utils.solvers import classical_natural_deduction_solver >>> derivation = classical_natural_deduction_solver.solve(classical_parser.parse("A → B, ~B / ~A")) >>> derivation.print_derivation(classical_parser) 0. A → B; premise; [] 1. ~B; premise; [] | 2. A; supposition; [] | 3. B; E→; [0, 2] | 4. ⊥; E~; [1, 3] 5. ~A; I~; [2, 4] >>> classical_natural_deduction_system.is_correct_derivation(derivation) True >>> # Also in first order! >>> from logics.utils.parsers import classical_predicate_parser >>> from logics.utils.solvers.first_order_natural_deduction import first_order_natural_deduction_solver >>> derivation = first_order_natural_deduction_solver.solve(classical_predicate_parser.parse('~∃x P(x) / ∀x ~P(x)')) >>> derivation.print_derivation(classical_predicate_parser) 0. ~∃x P(x); premise; [] | 1. P(a); supposition; [] | 2. ∃x P(x); I∃; [1] | 3. ⊥; E~; [0, 2] 4. ~P(a); I~; [1, 3] 5. ∀x ~P(x); I∀; [4]
I have now added tableaux systems:
>>> from logics.classes.propositional.proof_theories import TableauxNode >>> # Again, you can define your own tableaux system, here I use a predefined instance >>> from logics.instances.propositional.tableaux import classical_tableaux_system >>> n1 = TableauxNode(content=classical_parser.parse('~~~~p')) >>> n2 = TableauxNode(content=classical_parser.parse('~p'), parent=n1) >>> n3 = TableauxNode(content=classical_parser.parse('~~p'), justification='R~~', parent=n2) >>> n1.print_tree(classical_parser) (~~~p) └── ~p └── ~~p (R~~) >>> classical_tableaux_system.node_is_closed(n2) False >>> classical_tableaux_system.tree_is_closed(n1) True >>> classical_tableaux_system.rule_is_applicable(n1, 'R~~') True >>> classical_tableaux_system.is_correct_tree(n1) True >>> # The tableaux solver (unlike ND one) will work for any arbitrary system you define >>> tree = classical_tableaux_system.solve_tree(classical_parser.parse("~(p ∧ q) / ~p ∨ ~q")) >>> tree.print_tree(classical_parser) ~(p ∧ q) └── ~(~p ∨ ~q) ├── ~p (R~∧) │ └── ~~p (R~∨) │ └── ~~q (R~∨) └── ~q (R~∧) └── ~~p (R~∨) └── ~~q (R~∨) >>> # There is even a tableaux class for indexed tableaux, here is a predefined instance >>> from logics.instances.propositional.tableaux import LP_tableaux_system >>> tree2 = LP_tableaux_system.solve_tree(classical_parser.parse("~(p ∨ q) / ~~p ∧ ~~q")) >>> tree2.print_tree(classical_parser) ~(p ∨ q), 1 └── ~~p ∧ ~~q, 0 └── ~p ∧ ~q, 1 (R~∨1) ├── ~~p, 0 (R∧0) │ └── ~p, 1 (R∧1) │ └── ~q, 1 (R∧1) │ └── p, 0 (R~~0) └── ~~q, 0 (R∧0) └── ~p, 1 (R∧1) └── ~q, 1 (R∧1) └── q, 0 (R~~0)
And sequent calculi:
>>> sequent = classical_parser.parse("Gamma, A ==> B, Delta") >>> classical_parser.unparse(sequent) 'Γ, A ⇒ B, Δ' >>> sequent2 = sequent.substitute(language, "Γ", classical_parser.parse("D")) >>> classical_parser.unparse(sequent2) 'D, A ⇒ B, Δ' >>> # Again, you can define your sequent calculus, here I use a predefined instance >>> from logics.instances.propositional.sequents import LK >>> LK.sequent_is_axiom(classical_parser.parse("p or q ==> p or q")) True >>> from logics.classes.propositional.proof_theories import SequentNode >>> 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) # the root of the tree is the derived node Γ, A ⇒ A, Δ (WL) └── A ⇒ A, Δ (WR) └── A ⇒ A (identity) >>> LK.is_correct_tree(n1) True >>> LK.tree_is_closed(n3) True >>> # There is also a solver that will work whenever your system has no elimination rules >>> # A system that the solver can work with easily, see the docs for a description >>> from logics.instances.propositional.sequents import LKminEA >>> tree = LKminEA.reduce(classical_parser.parse("Gamma ==> A or ~A")) >>> tree.print_tree(classical_parser) Γ ⇒ A ∨ ~A (∨R1) └── Γ ⇒ A, ~A (~R) └── Γ, A ⇒ A (WL) └── A ⇒ A (identity)
There are also some predicate logic tools:
>>> from logics.classes.predicate.semantics import Model >>> model = Model({ ... 'domain': {1, 2}, ... 'a': 1, ... 'b': 2, ... 'P': {1}, ... 'R': {(1,1), (1,2)}, ... 'f': {((1,), 2), ((2,), 1)}, ... 'g': {((1, 1), 1), ((1, 2), 2), ((2, 1), 1), ((2, 2), 2)} ... }) >>> model.denotation('f') {((2,), 1), ((1,), 1)} >>> # Again, predefined instance, you can define this yourself >>> from logics.instances.predicate.model_semantics import classical_functional_model_semantics >>> classical_functional_model_semantics.valuation(parser.parse("P(a)"), model) '1' >>> classical_functional_model_semantics.valuation(parser.parse("R(a, b)"), model) '1' >>> classical_functional_model_semantics.valuation(parser.parse("R(f(a), g(f(a), b))"), model) '0' >>> classical_functional_model_semantics.valuation(parser.parse("exists x (P(f(x)))"), model) '1' >>> classical_functional_model_semantics.valuation(parser.parse("forall X (exists x (X(f(x))))"), model) '0' >>> # You can also define theories with fixed denotations for some terms by subclassing Model >>> from itertools import count >>> from logics.instances.predicate.model_subclasses import ArithmeticModel >>> from logics.utils.parsers.predicate_parser import arithmetic_parser >>> from logics.instances.predicate.model_semantics import arithmetic_model_semantics >>> arithmetic_model = ArithmeticModel({'domain': count(0)}) >>> arithmetic_model_semantics.valuation(arithmetic_parser.parse("s(0) > 0"), arithmetic_model) '1' >>> arithmetic_model_semantics.valuation(arithmetic_parser.parse("s(0) + s(0) = s(s(0))"), arithmetic_model) '1' >>> arithmetic_model_semantics.valuation(arithmetic_parser.parse("exists x (x = s(0))"), arithmetic_model) '1'
And many more things! (see the documentation)
Acknowledgements
logics is a project by Ariel Jonathan Roffé (CONICET / University of Buenos Aires)
Contributors to the project:
Joaquin S. Toranzo Calderon (mapped_logics module)
The author also wishes to thank the Buenos Aires Logic Group who supported this project.
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
File details
Details for the file logics-1.10.3.tar.gz
.
File metadata
- Download URL: logics-1.10.3.tar.gz
- Upload date:
- Size: 149.6 kB
- Tags: Source
- Uploaded using Trusted Publishing? No
- Uploaded via: twine/3.4.1 importlib_metadata/3.7.3 pkginfo/1.7.0 requests/2.25.0 requests-toolbelt/0.9.1 tqdm/4.59.0 CPython/3.10.12
File hashes
Algorithm | Hash digest | |
---|---|---|
SHA256 | 1b4da29fdeb0582f58751297e79d472137afea62d9fa29b6547256afca2f3a58 |
|
MD5 | 096e7750adb86368ea97c3e764987616 |
|
BLAKE2b-256 | 980897aa97c47659f55b539e4b34c118b0d79f2888408b87f518d3cf71f404d0 |
File details
Details for the file logics-1.10.3-py3-none-any.whl
.
File metadata
- Download URL: logics-1.10.3-py3-none-any.whl
- Upload date:
- Size: 169.1 kB
- Tags: Python 3
- Uploaded using Trusted Publishing? No
- Uploaded via: twine/3.4.1 importlib_metadata/3.7.3 pkginfo/1.7.0 requests/2.25.0 requests-toolbelt/0.9.1 tqdm/4.59.0 CPython/3.10.12
File hashes
Algorithm | Hash digest | |
---|---|---|
SHA256 | 61a447b10938dfae06383a6a26ce6fce419f0be2c3948bd560a4350763857540 |
|
MD5 | a176a0d3a5574f1fb540ac2582ee018a |
|
BLAKE2b-256 | 7bee8425a3767b1ee3d03bbb4f540e32a3ef979587063f49ee4ebc8f035ea2ee |