# Tensor Theorem Prover
[](https://github.com/chanind/tensor-theorem-prover)
[](https://codecov.io/gh/chanind/tensor-theorem-prover)
[](https://pypi.org/project/tensor-theorem-prover/)
[](https://tensor-theorem-prover.readthedocs.io/en/latest/?badge=latest)
First-order logic theorem prover supporting unification with approximate vector similarity
Full docs: https://tensor-theorem-prover.readthedocs.io
## Installation
```
pip install tensor-theorem-prover
```
## Usage
tensor-theorem-prover can be used either as a standard symbolic first-order theorem prover, or it can be used with vector embeddings and fuzzy unification.
The basic setup requires listing out first-order formulae, and using the `ResolutionProver` class to generate proofs.
```python
import numpy as np
from vector_theorem_prover import ResolutionProver, Constant, Predicate, Variable, Implies
X = Variable("X")
Y = Variable("Y")
Z = Variable("Z")
# predicates and constants can be given an embedding array for fuzzy unification
grandpa_of = Predicate("grandpa_of", np.array([1.0, 1.0, 0.0, 0.3, ...]))
grandfather_of = Predicate("grandfather_of", np.array([1.01, 0.95, 0.05, 0.33, ...]))
parent_of = Predicate("parent_of", np.array([ ... ]))
father_of = Predicate("father_of", np.array([ ... ]))
bart = Constant("bart", np.array([ ... ]))
homer = Constant("homer", np.array([ ... ]))
abe = Constant("abe", np.array([ ... ]))
knowledge = [
parent_of(homer, bart),
father_of(abe, homer),
# father_of(X, Z) ^ parent_of(Z, Y) -> grandpa_of(X, Y)
Implies(And(father_of(X, Z), parent_of(Z, Y)), grandpa_of(X, Y))
]
prover = ResolutionProver(knowledge=knowledge)
# query the prover to find who is bart's grandfather
proof = prover.prove(grandfather_of(X, bart))
# even though `grandpa_of` and `grandfather_of` are not identical symbols,
# their embedding is close enough that the prover can still find the answer
print(proof.substitutions[X]) # abe
# the prover will return `None` if a proof could not be found
failed_proof = prover.prove(grandfather_of(bart, homer))
print(failed_proof) # None
```
### Working with proof results
The `prover.prove()` method will return a `Proof` object if a successful proof is found. This object contains a list of all the resolutions, substitutions, and similarity calculations that went into proving the goal.
```python
proof = prover.prove(goal)
proof.substitutions # a map of all variables in the goal to their bound values
proof.similarity # the min similarity of all `unify` operations in this proof
proof.depth # the number of steps in this proof
proof.proof_steps # all the proof steps involved, including all resolutions and unifications along the way
```
The `Proof` object can be printed as a string to get a visual overview of the steps involved in the proof.
```python
X = Variable("X")
Y = Variable("Y")
father_of = Predicate("father_of")
parent_of = Predicate("parent_of")
is_male = Predicate("is_male")
bart = Constant("bart")
homer = Constant("homer")
knowledge = [
parent_of(homer, bart),
is_male(homer),
Implies(And(parent_of(X, Y), is_male(X)), father_of(X, Y)),
]
prover = ResolutionProver(knowledge=knowledge)
goal = father_of(homer, X)
proof = prover.prove(goal)
print(proof)
# Goal: [¬father_of(homer,X)]
# Subsitutions: {X -> bart}
# Similarity: 1.0
# Depth: 3
# Steps:
# Similarity: 1.0
# Source: [¬father_of(homer,X)]
# Target: [father_of(X,Y) ∨ ¬is_male(X) ∨ ¬parent_of(X,Y)]
# Unify: father_of(homer,X) = father_of(X,Y)
# Subsitutions: {}, {X -> homer, Y -> X}
# Resolvent: [¬is_male(homer) ∨ ¬parent_of(homer,X)]
# ---
# Similarity: 1.0
# Source: [¬is_male(homer) ∨ ¬parent_of(homer,X)]
# Target: [parent_of(homer,bart)]
# Unify: parent_of(homer,X) = parent_of(homer,bart)
# Subsitutions: {X -> bart}, {}
# Resolvent: [¬is_male(homer)]
# ---
# Similarity: 1.0
# Source: [¬is_male(homer)]
# Target: [is_male(homer)]
# Unify: is_male(homer) = is_male(homer)
# Subsitutions: {}, {}
# Resolvent: []
```
### Finding all possible proofs
The `prover.prove()` method will return the proof with the highest similarity score among all possible proofs, if one exists. If you want to get a list of all the possible proofs in descending order of similarity score, you can call `prover.prove_all()` to return a list of all proofs.
### Custom matching functions and similarity thresholds
By default, the prover will use cosine similarity for unification. If you'd like to use a different similarity function, you can pass in a function to the prover to perform the similarity calculation however you wish.
```python
def fancy_similarity(item1, item2):
norm = np.linalg.norm(item1.embedding) + np.linalg.norm(item2.embedding)
return np.linalg.norm(item1.embedding - item2.embedding) / norm
prover = ResolutionProver(knowledge=knowledge, similarity_func=fancy_similarity)
```
By default, there is a minimum similarity threshold of `0.5` for a unification to success. You can customize this as well when creating a `ResolutionProver` instance
```python
prover = ResolutionProver(knowledge=knowledge, min_similarity_threshold=0.9)
```
### Working with Tensors (Pytorch, Tensorflow, etc...)
By default, the similarity calculation assumes that the embeddings supplied for constants and predicates are numpy arrays. If you want to use tensors instead, this will work as long as you provide a `similarity_func` which can work with the tensor types you're using and return a float.
For example, if you're using Pytorch, it might look like the following:
```python
import torch
def torch_cosine_similarity(item1, item2):
similarity = torch.nn.functional.cosine_similarity(
item1.embedding,
item2.embedding,
0
)
return similarity.item()
prover = ResolutionProver(knowledge=knowledge, similarity_func=torch_cosine_similarity)
# for pytorch you may want to wrap the proving in torch.no_grad()
with torch.no_grad():
proof = prover.prove(goal)
```
### Max proof depth
By default, the ResolutionProver will abort proofs after a depth of 10. You can customize this behavior by passing `max_proof_depth` when creating the prover
```python
prover = ResolutionProver(knowledge=knowledge, max_proof_depth=10)
```
### Max resolvent width
By default, the ResolutionProver has no limit on how wide resolvents can get during the proving process. If the proofs are running too slowly, you can try to set `max_resolvent_width` to limit how many literals intermediate resolvents are allowed to contain. This should narrow the search tree, but has the trade-off of not finding proofs if the proof requires unifying together a lot of very wide clauses.
```python
prover = ResolutionProver(knowledge=knowledge, max_resolvent_width=10)
```
### Skipping seen resolvents
A major performance improvement when searching through a large proof space is to stop searching any branches that encounter a resolvent that's already been seen. Doing this is still guaranteed to find the proof with the highest similarity score, but it means the prover is no longer guaranteed to find every possible proof when running `prover.prove_all()`. Although, when dealing with anything beyond very small knowledge bases, finding every possible proof is likely not going to be computationally feasible anyway.
Searching for a proof using `prover.prove()` always enables this optimization, but you can enable it when using `prover.prove_all()` as well by passing the option `skip_seen_resolvents=True` when creating the `ResolutionProver`, like below:
```python
prover = ResolutionProver(knowledge=knowledge, skip_seen_resolvents=True)
```
### Max resolution attempts
As a final backstop against the search tree getting too large, you can set a maximum resolution attempts parameter to force the prover to give up after a finite amount of attempts. You can set this parameter when creating a `ResolutionProver` as shown below:
```python
prover = ResolutionProver(knowledge=knowledge, max_resolution_attempts=100_000_000)
```
### Multithreading
By default, the ResolutionProver will try to use available CPU cores up to a max of 6, though this may change in future releases. If you want to explicitly control the number of worker threads used for solving, pass `num_workers` when creating the `ResolutionProver`, like below:
```python
prover = ResolutionProver(knowledge=knowledge, num_workers=1)
```
## Acknowledgements
This library borrows code and ideas from the earier library [fuzzy-reasoner](https://github.com/fuzzy-reasoner/fuzzy-reasoner). The main difference between these libraries is that tensor-theorem-prover supports full first-order logic using Resolution, whereas fuzzy-reasoner is restricted to Horn clauses and uses backwards chaining. This library is also much more optimized than the fuzzy-reasoner, as the core of tensor-theorem-prover is written in rust and supports multithreading, while fuzzy-reasoner is pure Python.
Like fuzzy-reasoner, this library also takes inspiration from the following papers for the idea of using vector similarity in theorem proving:
- [End-to-End Differentiable Proving](https://arxiv.org/abs/1705.11040) by Rocktäschel et al.
- [Braid - Weaving Symbolic and Neural Knowledge into Coherent Logical Explanations](https://arxiv.org/abs/2011.13354) by Kalyanpur et al.
## Contributing
Contributions are welcome! Please leave an issue in the Github repo if you find any bugs, and open a pull request with and fixes or improvements that you'd like to contribute.
Raw data
{
"_id": null,
"home_page": "https://github.com/chanind/tensor-theorem-prover",
"name": "tensor-theorem-prover",
"maintainer": "",
"docs_url": null,
"requires_python": ">=3.8.1,<4.0",
"maintainer_email": "",
"keywords": "theorem-proving,logic,first-order,unification,reasoning",
"author": "David Chanin",
"author_email": "chanindav@gmail.com",
"download_url": "https://files.pythonhosted.org/packages/ce/c0/16f418092bf56bf0fcbe1cdc4b30e7fca6dea77c2dc7f487da320941b3d5/tensor_theorem_prover-0.14.0.tar.gz",
"platform": null,
"description": "# Tensor Theorem Prover\n\n[](https://github.com/chanind/tensor-theorem-prover)\n[](https://codecov.io/gh/chanind/tensor-theorem-prover)\n[](https://pypi.org/project/tensor-theorem-prover/)\n[](https://tensor-theorem-prover.readthedocs.io/en/latest/?badge=latest)\n\nFirst-order logic theorem prover supporting unification with approximate vector similarity\n\nFull docs: https://tensor-theorem-prover.readthedocs.io\n\n## Installation\n\n```\npip install tensor-theorem-prover\n```\n\n## Usage\n\ntensor-theorem-prover can be used either as a standard symbolic first-order theorem prover, or it can be used with vector embeddings and fuzzy unification.\n\nThe basic setup requires listing out first-order formulae, and using the `ResolutionProver` class to generate proofs.\n\n```python\nimport numpy as np\nfrom vector_theorem_prover import ResolutionProver, Constant, Predicate, Variable, Implies\n\nX = Variable(\"X\")\nY = Variable(\"Y\")\nZ = Variable(\"Z\")\n# predicates and constants can be given an embedding array for fuzzy unification\ngrandpa_of = Predicate(\"grandpa_of\", np.array([1.0, 1.0, 0.0, 0.3, ...]))\ngrandfather_of = Predicate(\"grandfather_of\", np.array([1.01, 0.95, 0.05, 0.33, ...]))\nparent_of = Predicate(\"parent_of\", np.array([ ... ]))\nfather_of = Predicate(\"father_of\", np.array([ ... ]))\nbart = Constant(\"bart\", np.array([ ... ]))\nhomer = Constant(\"homer\", np.array([ ... ]))\nabe = Constant(\"abe\", np.array([ ... ]))\n\nknowledge = [\n parent_of(homer, bart),\n father_of(abe, homer),\n # father_of(X, Z) ^ parent_of(Z, Y) -> grandpa_of(X, Y)\n Implies(And(father_of(X, Z), parent_of(Z, Y)), grandpa_of(X, Y))\n]\n\nprover = ResolutionProver(knowledge=knowledge)\n\n# query the prover to find who is bart's grandfather\nproof = prover.prove(grandfather_of(X, bart))\n\n# even though `grandpa_of` and `grandfather_of` are not identical symbols,\n# their embedding is close enough that the prover can still find the answer\nprint(proof.substitutions[X]) # abe\n\n# the prover will return `None` if a proof could not be found\nfailed_proof = prover.prove(grandfather_of(bart, homer))\nprint(failed_proof) # None\n\n```\n\n### Working with proof results\n\nThe `prover.prove()` method will return a `Proof` object if a successful proof is found. This object contains a list of all the resolutions, substitutions, and similarity calculations that went into proving the goal.\n\n```python\nproof = prover.prove(goal)\n\nproof.substitutions # a map of all variables in the goal to their bound values\nproof.similarity # the min similarity of all `unify` operations in this proof\nproof.depth # the number of steps in this proof\nproof.proof_steps # all the proof steps involved, including all resolutions and unifications along the way\n```\n\nThe `Proof` object can be printed as a string to get a visual overview of the steps involved in the proof.\n\n```python\nX = Variable(\"X\")\nY = Variable(\"Y\")\nfather_of = Predicate(\"father_of\")\nparent_of = Predicate(\"parent_of\")\nis_male = Predicate(\"is_male\")\nbart = Constant(\"bart\")\nhomer = Constant(\"homer\")\n\nknowledge = [\n parent_of(homer, bart),\n is_male(homer),\n Implies(And(parent_of(X, Y), is_male(X)), father_of(X, Y)),\n]\n\nprover = ResolutionProver(knowledge=knowledge)\n\ngoal = father_of(homer, X)\nproof = prover.prove(goal)\n\nprint(proof)\n# Goal: [\u00acfather_of(homer,X)]\n# Subsitutions: {X -> bart}\n# Similarity: 1.0\n# Depth: 3\n# Steps:\n# Similarity: 1.0\n# Source: [\u00acfather_of(homer,X)]\n# Target: [father_of(X,Y) \u2228 \u00acis_male(X) \u2228 \u00acparent_of(X,Y)]\n# Unify: father_of(homer,X) = father_of(X,Y)\n# Subsitutions: {}, {X -> homer, Y -> X}\n# Resolvent: [\u00acis_male(homer) \u2228 \u00acparent_of(homer,X)]\n# ---\n# Similarity: 1.0\n# Source: [\u00acis_male(homer) \u2228 \u00acparent_of(homer,X)]\n# Target: [parent_of(homer,bart)]\n# Unify: parent_of(homer,X) = parent_of(homer,bart)\n# Subsitutions: {X -> bart}, {}\n# Resolvent: [\u00acis_male(homer)]\n# ---\n# Similarity: 1.0\n# Source: [\u00acis_male(homer)]\n# Target: [is_male(homer)]\n# Unify: is_male(homer) = is_male(homer)\n# Subsitutions: {}, {}\n# Resolvent: []\n```\n\n### Finding all possible proofs\n\nThe `prover.prove()` method will return the proof with the highest similarity score among all possible proofs, if one exists. If you want to get a list of all the possible proofs in descending order of similarity score, you can call `prover.prove_all()` to return a list of all proofs.\n\n### Custom matching functions and similarity thresholds\n\nBy default, the prover will use cosine similarity for unification. If you'd like to use a different similarity function, you can pass in a function to the prover to perform the similarity calculation however you wish.\n\n```python\ndef fancy_similarity(item1, item2):\n norm = np.linalg.norm(item1.embedding) + np.linalg.norm(item2.embedding)\n return np.linalg.norm(item1.embedding - item2.embedding) / norm\n\nprover = ResolutionProver(knowledge=knowledge, similarity_func=fancy_similarity)\n```\n\nBy default, there is a minimum similarity threshold of `0.5` for a unification to success. You can customize this as well when creating a `ResolutionProver` instance\n\n```python\nprover = ResolutionProver(knowledge=knowledge, min_similarity_threshold=0.9)\n```\n\n### Working with Tensors (Pytorch, Tensorflow, etc...)\n\nBy default, the similarity calculation assumes that the embeddings supplied for constants and predicates are numpy arrays. If you want to use tensors instead, this will work as long as you provide a `similarity_func` which can work with the tensor types you're using and return a float.\n\nFor example, if you're using Pytorch, it might look like the following:\n\n```python\nimport torch\n\ndef torch_cosine_similarity(item1, item2):\n similarity = torch.nn.functional.cosine_similarity(\n item1.embedding,\n item2.embedding,\n 0\n )\n return similarity.item()\n\nprover = ResolutionProver(knowledge=knowledge, similarity_func=torch_cosine_similarity)\n\n# for pytorch you may want to wrap the proving in torch.no_grad()\nwith torch.no_grad():\n proof = prover.prove(goal)\n```\n\n### Max proof depth\n\nBy default, the ResolutionProver will abort proofs after a depth of 10. You can customize this behavior by passing `max_proof_depth` when creating the prover\n\n```python\nprover = ResolutionProver(knowledge=knowledge, max_proof_depth=10)\n```\n\n### Max resolvent width\n\nBy default, the ResolutionProver has no limit on how wide resolvents can get during the proving process. If the proofs are running too slowly, you can try to set `max_resolvent_width` to limit how many literals intermediate resolvents are allowed to contain. This should narrow the search tree, but has the trade-off of not finding proofs if the proof requires unifying together a lot of very wide clauses.\n\n```python\nprover = ResolutionProver(knowledge=knowledge, max_resolvent_width=10)\n```\n\n### Skipping seen resolvents\n\nA major performance improvement when searching through a large proof space is to stop searching any branches that encounter a resolvent that's already been seen. Doing this is still guaranteed to find the proof with the highest similarity score, but it means the prover is no longer guaranteed to find every possible proof when running `prover.prove_all()`. Although, when dealing with anything beyond very small knowledge bases, finding every possible proof is likely not going to be computationally feasible anyway.\n\nSearching for a proof using `prover.prove()` always enables this optimization, but you can enable it when using `prover.prove_all()` as well by passing the option `skip_seen_resolvents=True` when creating the `ResolutionProver`, like below:\n\n```python\nprover = ResolutionProver(knowledge=knowledge, skip_seen_resolvents=True)\n```\n\n### Max resolution attempts\n\nAs a final backstop against the search tree getting too large, you can set a maximum resolution attempts parameter to force the prover to give up after a finite amount of attempts. You can set this parameter when creating a `ResolutionProver` as shown below:\n\n```python\nprover = ResolutionProver(knowledge=knowledge, max_resolution_attempts=100_000_000)\n```\n\n### Multithreading\n\nBy default, the ResolutionProver will try to use available CPU cores up to a max of 6, though this may change in future releases. If you want to explicitly control the number of worker threads used for solving, pass `num_workers` when creating the `ResolutionProver`, like below:\n\n```python\nprover = ResolutionProver(knowledge=knowledge, num_workers=1)\n```\n\n## Acknowledgements\n\nThis library borrows code and ideas from the earier library [fuzzy-reasoner](https://github.com/fuzzy-reasoner/fuzzy-reasoner). The main difference between these libraries is that tensor-theorem-prover supports full first-order logic using Resolution, whereas fuzzy-reasoner is restricted to Horn clauses and uses backwards chaining. This library is also much more optimized than the fuzzy-reasoner, as the core of tensor-theorem-prover is written in rust and supports multithreading, while fuzzy-reasoner is pure Python.\n\nLike fuzzy-reasoner, this library also takes inspiration from the following papers for the idea of using vector similarity in theorem proving:\n\n- [End-to-End Differentiable Proving](https://arxiv.org/abs/1705.11040) by Rockt\u00e4schel et al.\n- [Braid - Weaving Symbolic and Neural Knowledge into Coherent Logical Explanations](https://arxiv.org/abs/2011.13354) by Kalyanpur et al.\n\n## Contributing\n\nContributions are welcome! Please leave an issue in the Github repo if you find any bugs, and open a pull request with and fixes or improvements that you'd like to contribute.\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "Customizable first-order logic theorem prover supporting approximate vector similarity in unification",
"version": "0.14.0",
"split_keywords": [
"theorem-proving",
"logic",
"first-order",
"unification",
"reasoning"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "8945a0c9a8a6151489b3873b3cf07fbf81b5b45b0dc60559c2a370f4792b065c",
"md5": "ae7bc27a7b203e464607d2e0c60fcff3",
"sha256": "5f72b418d01580c61b31fd0c00bca757b41cb0d9cd71df4dbaf89b53b311b124"
},
"downloads": -1,
"filename": "tensor_theorem_prover-0.14.0-cp38-cp38-macosx_10_7_x86_64.whl",
"has_sig": false,
"md5_digest": "ae7bc27a7b203e464607d2e0c60fcff3",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8.1,<4.0",
"size": 902709,
"upload_time": "2023-02-07T17:24:14",
"upload_time_iso_8601": "2023-02-07T17:24:14.648949Z",
"url": "https://files.pythonhosted.org/packages/89/45/a0c9a8a6151489b3873b3cf07fbf81b5b45b0dc60559c2a370f4792b065c/tensor_theorem_prover-0.14.0-cp38-cp38-macosx_10_7_x86_64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "e20ca0e7339552c2553c82e6ed1a1c0409bff56df011c4b59ecbe327c20bf400",
"md5": "45e20a94a1fb3e4eecc06998becec649",
"sha256": "b29817d44332fc040618fea3b4c3b4c76d78adf53f787e45f619eb2e8ec7ea4a"
},
"downloads": -1,
"filename": "tensor_theorem_prover-0.14.0-cp38-cp38-macosx_10_9_x86_64.macosx_11_0_arm64.macosx_10_9_universal2.whl",
"has_sig": false,
"md5_digest": "45e20a94a1fb3e4eecc06998becec649",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8.1,<4.0",
"size": 1714707,
"upload_time": "2023-02-07T17:24:16",
"upload_time_iso_8601": "2023-02-07T17:24:16.610435Z",
"url": "https://files.pythonhosted.org/packages/e2/0c/a0e7339552c2553c82e6ed1a1c0409bff56df011c4b59ecbe327c20bf400/tensor_theorem_prover-0.14.0-cp38-cp38-macosx_10_9_x86_64.macosx_11_0_arm64.macosx_10_9_universal2.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "61ab2962eb257f44c7cc886c21ac1b90a45d4930e4adfd916e3d621b54c653a7",
"md5": "52b69e718d298095f63de8a25edbd7f5",
"sha256": "d6215ff770fa3bb580ad38d7cd0504c89827b560e0321bf8da104cd7f415afaf"
},
"downloads": -1,
"filename": "tensor_theorem_prover-0.14.0-cp38-cp38-manylinux_2_12_i686.manylinux2010_i686.whl",
"has_sig": false,
"md5_digest": "52b69e718d298095f63de8a25edbd7f5",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8.1,<4.0",
"size": 1823776,
"upload_time": "2023-02-07T17:24:18",
"upload_time_iso_8601": "2023-02-07T17:24:18.147264Z",
"url": "https://files.pythonhosted.org/packages/61/ab/2962eb257f44c7cc886c21ac1b90a45d4930e4adfd916e3d621b54c653a7/tensor_theorem_prover-0.14.0-cp38-cp38-manylinux_2_12_i686.manylinux2010_i686.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "9393ed422925fcac337654b1c05de6a931ab8d890cb51a390d77fac45b584b77",
"md5": "a47676e27710be30288d6df19bd5ba26",
"sha256": "feeac8c591e8eebc9e542eca60f23c856049f4c20cf05a57343f2f49c656799b"
},
"downloads": -1,
"filename": "tensor_theorem_prover-0.14.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl",
"has_sig": false,
"md5_digest": "a47676e27710be30288d6df19bd5ba26",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8.1,<4.0",
"size": 1825696,
"upload_time": "2023-02-07T17:24:20",
"upload_time_iso_8601": "2023-02-07T17:24:20.277779Z",
"url": "https://files.pythonhosted.org/packages/93/93/ed422925fcac337654b1c05de6a931ab8d890cb51a390d77fac45b584b77/tensor_theorem_prover-0.14.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "81f8f0287201a15a0dc0d509559b50e33102ff188b9bc9e301587fe4456f0bee",
"md5": "306eae88b1ef148369a1c1bbc3a292fc",
"sha256": "8f8c589196579120e39d7642a879410cdfd34cbd4b836d5594b41755310a9c57"
},
"downloads": -1,
"filename": "tensor_theorem_prover-0.14.0-cp38-cp38-musllinux_1_2_aarch64.whl",
"has_sig": false,
"md5_digest": "306eae88b1ef148369a1c1bbc3a292fc",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8.1,<4.0",
"size": 1949614,
"upload_time": "2023-02-07T17:24:21",
"upload_time_iso_8601": "2023-02-07T17:24:21.991944Z",
"url": "https://files.pythonhosted.org/packages/81/f8/f0287201a15a0dc0d509559b50e33102ff188b9bc9e301587fe4456f0bee/tensor_theorem_prover-0.14.0-cp38-cp38-musllinux_1_2_aarch64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "352cc74acb14fb783a446594fbe2a5589a5e1b5aa979a676bd044f992e7e55af",
"md5": "0547ec904c1258f62f46d2f81124fd2f",
"sha256": "922b21f16d54ff585c3a3d5e486031be49036438b509163e9f7818cfd239e095"
},
"downloads": -1,
"filename": "tensor_theorem_prover-0.14.0-cp38-cp38-musllinux_1_2_armv7l.whl",
"has_sig": false,
"md5_digest": "0547ec904c1258f62f46d2f81124fd2f",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8.1,<4.0",
"size": 1990234,
"upload_time": "2023-02-07T17:24:23",
"upload_time_iso_8601": "2023-02-07T17:24:23.839051Z",
"url": "https://files.pythonhosted.org/packages/35/2c/c74acb14fb783a446594fbe2a5589a5e1b5aa979a676bd044f992e7e55af/tensor_theorem_prover-0.14.0-cp38-cp38-musllinux_1_2_armv7l.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "1034236f779f29f1f6e639e5c3ae8999f77eed2a8b7fc31154d8fa3ec33408b9",
"md5": "fe0f86f6c47cb410f092aa0ba40fc2f7",
"sha256": "1b3f37a3772d532c1a231a18e5cf7857c2989aafd66f9b32aaf421f6430fee80"
},
"downloads": -1,
"filename": "tensor_theorem_prover-0.14.0-cp38-cp38-musllinux_1_2_i686.whl",
"has_sig": false,
"md5_digest": "fe0f86f6c47cb410f092aa0ba40fc2f7",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8.1,<4.0",
"size": 1962003,
"upload_time": "2023-02-07T17:24:25",
"upload_time_iso_8601": "2023-02-07T17:24:25.322412Z",
"url": "https://files.pythonhosted.org/packages/10/34/236f779f29f1f6e639e5c3ae8999f77eed2a8b7fc31154d8fa3ec33408b9/tensor_theorem_prover-0.14.0-cp38-cp38-musllinux_1_2_i686.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "20eef455947b38139a5232e807050a462d3a7f9fd7d524119c362ff11ee57418",
"md5": "98c7e5c9582c957a07e8a61f32a8ed21",
"sha256": "0c8407daaa90da7b91a43fa586f04ed4e48ad79f563ad1e88db58829d71d121f"
},
"downloads": -1,
"filename": "tensor_theorem_prover-0.14.0-cp38-cp38-musllinux_1_2_x86_64.whl",
"has_sig": false,
"md5_digest": "98c7e5c9582c957a07e8a61f32a8ed21",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8.1,<4.0",
"size": 1993977,
"upload_time": "2023-02-07T17:24:27",
"upload_time_iso_8601": "2023-02-07T17:24:27.276178Z",
"url": "https://files.pythonhosted.org/packages/20/ee/f455947b38139a5232e807050a462d3a7f9fd7d524119c362ff11ee57418/tensor_theorem_prover-0.14.0-cp38-cp38-musllinux_1_2_x86_64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "bc5a97d3039c17bcb67390e6e6ed08868c7b108b2db09173a22339983c3d55e6",
"md5": "bdd73cddafd382427931e097d5d167b3",
"sha256": "d2f2c586f8c0af5bc567be1306771dff3aec06336514e4b3432eaa4fee0d8338"
},
"downloads": -1,
"filename": "tensor_theorem_prover-0.14.0-cp38-none-win32.whl",
"has_sig": false,
"md5_digest": "bdd73cddafd382427931e097d5d167b3",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8.1,<4.0",
"size": 626309,
"upload_time": "2023-02-07T17:24:28",
"upload_time_iso_8601": "2023-02-07T17:24:28.483753Z",
"url": "https://files.pythonhosted.org/packages/bc/5a/97d3039c17bcb67390e6e6ed08868c7b108b2db09173a22339983c3d55e6/tensor_theorem_prover-0.14.0-cp38-none-win32.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "e6b74c303c9f2165be7ed205446b605a95210d66ea882b13b0e145e9721aa9b5",
"md5": "880262a45c113f48cd1e467afdac8c29",
"sha256": "b34e79a1fe8cbf6301b32455cf15e694f9156268226e8b3e61bf6c476f1940ba"
},
"downloads": -1,
"filename": "tensor_theorem_prover-0.14.0-cp38-none-win_amd64.whl",
"has_sig": false,
"md5_digest": "880262a45c113f48cd1e467afdac8c29",
"packagetype": "bdist_wheel",
"python_version": "cp38",
"requires_python": ">=3.8.1,<4.0",
"size": 694096,
"upload_time": "2023-02-07T17:24:29",
"upload_time_iso_8601": "2023-02-07T17:24:29.741982Z",
"url": "https://files.pythonhosted.org/packages/e6/b7/4c303c9f2165be7ed205446b605a95210d66ea882b13b0e145e9721aa9b5/tensor_theorem_prover-0.14.0-cp38-none-win_amd64.whl",
"yanked": false,
"yanked_reason": null
},
{
"comment_text": "",
"digests": {
"blake2b_256": "cec016f418092bf56bf0fcbe1cdc4b30e7fca6dea77c2dc7f487da320941b3d5",
"md5": "6870b72db0f706230264af9c720ecc39",
"sha256": "aa5e121c235ac3d6b56961ff92721f8f5c25f7a8a9c0b8539f3e448a7f32d4a7"
},
"downloads": -1,
"filename": "tensor_theorem_prover-0.14.0.tar.gz",
"has_sig": false,
"md5_digest": "6870b72db0f706230264af9c720ecc39",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.8.1,<4.0",
"size": 3073261,
"upload_time": "2023-02-07T17:24:31",
"upload_time_iso_8601": "2023-02-07T17:24:31.105136Z",
"url": "https://files.pythonhosted.org/packages/ce/c0/16f418092bf56bf0fcbe1cdc4b30e7fca6dea77c2dc7f487da320941b3d5/tensor_theorem_prover-0.14.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2023-02-07 17:24:31",
"github": true,
"gitlab": false,
"bitbucket": false,
"github_user": "chanind",
"github_project": "tensor-theorem-prover",
"travis_ci": false,
"coveralls": true,
"github_actions": true,
"lcname": "tensor-theorem-prover"
}
JSON
