Algebraic Structures

Axiom Checkers

residuated_binars.axiom_checkers.absorbs(table1: Dict[str, Dict[str, str]], table2: Dict[str, Dict[str, str]]) → bool

Check an absorption law.

>>> conjunction = {"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "1"}}
>>> disjunction = {"0": {"0": "0", "1": "1"}, "1": {"0": "1", "1": "1"}}
>>> absorbs(conjunction, disjunction)
True
>>> absorbs(conjunction, conjunction)
False
Parameters

  • table1 – a multiplication table of a binary operation

  • table2 – a multiplication table of another binary operation

Returns

whether the absorption law is true with respect to two binary operation

residuated_binars.axiom_checkers.associative(cayley_table: Dict[str, Dict[str, str]]) → bool

Check associativity.

>>> associative({"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "0"}})
True
>>> associative({"0": {"0": "1", "1": "0"}, "1": {"0": "0", "1": "0"}})
False
Parameters

cayley_table – a multiplication table of a binary operation

Returns

whether the operation is associative or not

residuated_binars.axiom_checkers.commutative(cayley_table: Dict[str, Dict[str, str]]) → bool

Check commutativity.

>>> commutative({"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "0"}})
True
>>> commutative({"0": {"0": "0", "1": "1"}, "1": {"0": "0", "1": "0"}})
False
Parameters

cayley_table – a multiplication table of a binary operation

Returns

whether the operation is commutative or not

residuated_binars.axiom_checkers.idempotent(cayley_table: Dict[str, Dict[str, str]]) → bool

Check idempotency.

>>> idempotent({"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "1"}})
True
>>> idempotent({"0": {"0": "0", "1": "1"}, "1": {"0": "0", "1": "0"}})
False
Parameters

cayley_table – a multiplication table of a binary operation

Returns

whether the operation is idempotent or not

residuated_binars.axiom_checkers.is_left_identity(cayley_table: Dict[str, Dict[str, str]], identity: str) → bool

Check left identity.

>>> is_left_identity(
...     {"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "1"}}, "1"
... )
True
>>> is_left_identity(
...     {"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "1"}}, "0"
... )
False
Parameters

  • cayley_table – a multiplication table of a binary operation

  • identity – a symbol for identity

Returns

whether identity is a left identity for a Cayley table

residuated_binars.axiom_checkers.is_left_inverse(cayley_table: Dict[str, Dict[str, str]], inverse: Dict[str, str], identity: str) → bool

Check left inverse.

>>> op = {"0": {"0": "1", "1": "1"}, "1": {"0": "1", "1": "1"}}
>>> inv = {"0": "1", "1": "1"}
>>> is_left_inverse(op, inv, "1")
True
>>> is_left_inverse(op, inv, "0")
False
Parameters

  • cayley_table – a multiplication table of a binary operation

  • inverse – a map for the operation of inversion

  • identity – a symbol for identity

Returns

whether inverse is a left inverse for a Cayley table

residuated_binars.axiom_checkers.is_left_zero(cayley_table: Dict[str, Dict[str, str]], zero: str) → bool

Check left zero.

>>> table = {"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "1"}}
>>> is_left_zero(table, "0")
True
>>> is_left_zero(table, "1")
False
Parameters

  • cayley_table – a multiplication table of a binary operation

  • zero – a symbol for the zero

Returns

whether zero is a left zero for a Cayley table

residuated_binars.axiom_checkers.is_right_identity(cayley_table: Dict[str, Dict[str, str]], identity: str) → bool

Check right identity.

>>> is_right_identity(
...     {"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "1"}}, "1"
... )
True
>>> is_right_identity(
...     {"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "1"}}, "0"
... )
False
Parameters

  • cayley_table – a multiplication table of a binary operation

  • identity – a symbol for identity

Returns

whether identity is a right identity for a Cayley table

residuated_binars.axiom_checkers.is_right_inverse(cayley_table: Dict[str, Dict[str, str]], inverse: Dict[str, str], identity: str) → bool

Check right inverse.

>>> op = {"0": {"0": "1", "1": "1"}, "1": {"0": "1", "1": "1"}}
>>> inv = {"0": "1", "1": "1"}
>>> is_right_inverse(op, inv, "1")
True
>>> is_right_inverse(op, inv, "0")
False
Parameters

  • cayley_table – a multiplication table of a binary operation

  • inverse – a map for the operation of inversion

  • identity – a symbol for identity

Returns

whether inverse is a right inverse for a Cayley table

residuated_binars.axiom_checkers.is_right_zero(cayley_table: Dict[str, Dict[str, str]], zero: str) → bool

Check right zero.

>>> table = {"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "1"}}
>>> is_right_zero(table, "0")
True
>>> is_right_zero(table, "1")
False
Parameters

  • cayley_table – a multiplication table of a binary operation

  • zero – a symbol for the zero

Returns

whether zero is a right zero for a Cayley table

residuated_binars.axiom_checkers.left_distributive(table1: Dict[str, Dict[str, str]], table2: Dict[str, Dict[str, str]]) → bool

Check left distributivity.

>>> operation = {"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "0"}}
>>> left_distributive(operation, operation)
True
>>> operation = {"0": {"0": "1", "1": "0"}, "1": {"0": "0", "1": "0"}}
>>> left_distributive(operation, operation)
False
Parameters

  • table1 – a multiplication table of a binary operation

  • table2 – a multiplication table of another binary operation

Returns

whether the first operation is left distributive with respect to the second one or not

residuated_binars.axiom_checkers.right_distributive(table1: Dict[str, Dict[str, str]], table2: Dict[str, Dict[str, str]]) → bool

Check right distributivity.

>>> operation = {"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "0"}}
>>> right_distributive(operation, operation)
True
>>> operation = {"0": {"0": "0", "1": "1"}, "1": {"0": "0", "1": "0"}}
>>> right_distributive(operation, operation)
False
Parameters

  • table1 – a multiplication table of a binary operation

  • table2 – a multiplication table of another binary operation

Returns

whether the first operation is right distributive with respect to the second one or not

Parser

residuated_binars.parser.choose_algebraic_structure(label: str, operations: Dict[str, Dict[str, Any]]) → AlgebraicStructure

Decide in which algebraic structure to saved the parsed result.

Parameters

  • label – a name of that particular algebraic structure example

  • operations – a dictionary of unary and binary operations

Returns

an algebraic structure of a concrete type ( depending on the signature)

residuated_binars.parser.isabelle_format_to_algebra(isabelle_message: str, label: str) → AlgebraicStructure

Parse the textual representation of operations to AlgebraicStructure.

Parameters

  • isabelle_message – a body of reply from Isabelle server (in JSON)

  • label – a name of the theory for which we got a reply from server

Returns

a residuated binar

residuated_binars.parser.isabelle_response_to_algebra(filename: str) → List[AlgebraicStructure]

Read file with replies from isabelle server and parse them.

>>> import sys
>>> if sys.version_info.major == 3 and sys.version_info.minor >= 9:
...     from importlib.resources import files
... else:
...     from importlib_resources import files
>>> import os
>>> len(isabelle_response_to_algebra(
...     files("residuated_binars")
...     .joinpath(os.path.join("resources", "isabelle2.out"))
... ))
6
Parameters

filename – a name of a file to which all replies from Isabelle server where written

Returns

a list of algebraic structures

residuated_binars.parser.parse_binary_operation(line: str) → Dict[str, Dict[str, str]]

Parse text describing a binary operation in Isabelle server response.

Parameters

line – a part of Isabelle server response, representing a binary operation

Returns

a Cayley table

residuated_binars.parser.parse_unary_operation(line: str) → Dict[str, str]

Parse text describing a unary operation in Isabelle server response.

Parameters

line – a part of Isabelle server response, representing an unary operation

Returns

an inner representation of an unary operation

Algebraic Structure

class residuated_binars.algebraic_structure.AlgebraicStructure(label: str, operations: Dict[str, Dict[str, Any]])

A base class for difference algebraic structures.

>>> magma_with_involution = AlgebraicStructure(
...     label="test",
...     operations={
...         "mult": {"0": {"0": "0", "1": "1"}, "1": {"0": "1", "1": "1"}},
...         "invo": {"0": "1", "1": "0"}
...     }
... )
>>> magma_with_involution
{'mult': [[0, 1], [1, 1]], 'invo': [1, 0]}
>>> magma_with_involution.symbols
['0', '1']
>>> magma_with_involution.remap_symbols({"0": "c1", "1": "c2"})
>>> magma_with_involution
{'mult': [[0, 1], [1, 1]], 'invo': [1, 0]}
>>> magma_with_involution.symbols
['c1', 'c2']
>>> print(magma_with_involution.mace4_format)
mult(c1, c1) = c1.
mult(c1, c2) = c2.
mult(c2, c1) = c2.
mult(c2, c2) = c2.
invo(c1) = c2.
invo(c2) = c1.

>>> class Magma(AlgebraicStructure):
...     ''' an example with redefined operation symbol '''
...
...     @property
...     def operation_map(self) -> Dict[str, str]:
...         return {"mult": "*"}
>>> magma = Magma("test", {"mult": {"c": {"c": "c"}}})
>>> print(magma.mace4_format)
c * c = c.
property cardinality: int

Return the number of items in the algebraic structure.

check_axioms() → None

Check axioms specific to that algebraic structure.

If any axiom fails, raise an error.

property mace4_format: str

Represent the algebraic structure in Prover9/Mace4 format.

Returns

a string representation

property operation_map: Dict[str, str]

Return a map from operation labels to operation symbols.

Labels are used for the infix notation and symbols —

for functional one.

remap_symbols(symbol_map: Dict[str, str]) → None

Rename symbols in a given way.

Parameters

symbol_map – what map to what

property symbols: List[str]

Return a list of symbols denoting items of an the structure.

property tabular_format: Dict[str, Union[List[List[int]], List[int]]]

Return a dictionary of Cayley tables as lists of lists.

Lattice

class residuated_binars.lattice.Lattice(label: str, operations: Dict[str, Dict[str, Any]])

A representation of a lattice.

>>> join = {"0": {"0": "0", "1": "1"}, "1": {"0": "1", "1": "1"}}
>>> meet = {"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "1"}}
>>> lattice = Lattice("test", {"join": join, "meet": meet})
>>> print(lattice.mace4_format)
0 v 0 = 0.
0 v 1 = 1.
1 v 0 = 1.
1 v 1 = 1.
0 ^ 0 = 0.
0 ^ 1 = 0.
1 ^ 0 = 0.
1 ^ 1 = 1.

>>> lattice.canonise_symbols()
>>> print(lattice.graphviz_repr)
graph {
    "⟙" -- "⟘"
}
>>> join["0"]["1"] = "0"
>>> Lattice("test", {"join": join, "meet": meet})
Traceback (most recent call last):
 ...
ValueError: join is not commutative
>>> join["0"]["1"] = "1"
>>> meet["0"]["1"] = "1"
>>> Lattice("test", {"join": join, "meet": meet})
Traceback (most recent call last):
 ...
ValueError: meet is not commutative
>>> meet["0"]["1"] = "0"
>>> join["0"]["0"] = "1"
>>> Lattice("test", {"join": join, "meet": meet})
Traceback (most recent call last):
 ...
ValueError: absorption laws fail
>>> join = {'0': {'0': '1', '1': '0'}, '1': {'0': '0', '1': '0'}}
>>> meet = {'0': {'0': '0', '1': '0'}, '1': {'0': '0', '1': '1'}}
>>> Lattice("test", {"join": join, "meet": meet})
Traceback (most recent call last):
 ...
ValueError: join is not associative
>>> join = {'0': {'0': '0', '1': '0'}, '1': {'0': '0', '1': '1'}}
>>> meet = {'0': {'0': '1', '1': '0'}, '1': {'0': '0', '1': '0'}}
>>> Lattice("test", {"join": join, "meet": meet})
Traceback (most recent call last):
 ...
ValueError: meet is not associative
canonise_symbols() → None

Enumerate lattice’s items in a canonical way.

check_axioms() → None

Check axioms specific to that algebraic structure.

If any axiom fails, raise an error.

property graphviz_repr: str

Return a representation usable by graphviz of Hasse diagram.

property hasse: List[Tuple[str, str]]

Return a representation of a Hasse diagram of a lattice.

property more: Dict[str, List[str]]

Return a representation of a ‘more’ relation of the lattice.

property operation_map: Dict[str, str]

Return a map from operation labels to operation symbols.

Labels are used for the infix notation and symbols —

for functional one.

Residuated Binar

class residuated_binars.residuated_binar.ResiduatedBinar(label: str, operations: Dict[str, Dict[str, Any]])

A representation of a residuated binar (with involution).

>>> join = {"0": {"0": "0", "1": "1"}, "1": {"0": "1", "1": "1"}}
>>> meet = {"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "1"}}
>>> mult = {"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "0"}}
>>> const = {"0": {"0": "1", "1": "1"}, "1": {"0": "1", "1": "1"}}
>>> binar = ResiduatedBinar(
...     label="test",
...     operations={
...         "join": join, "meet": meet, "mult": mult, "over": const,
...         "undr": const, "invo": {"0": "1", "1": "0"}
...     }
... )
>>> print(binar.latex_mult_table)
\begin{table}[]
\begin{tabular}{l|ll}
$\cdot$ & $0$ & $1$\\\hline
$0$ & $0$ & $0$ & \\
$1$ & $0$ & $0$ & \\
\end{tabular}
\end{table}

>>> print(binar.markdown_mult_table)
|*|0|1|
|-|-|-|
|**0**|0|0|
|**1**|0|0|

>>> mult["0"]["0"] = "1"
>>> ResiduatedBinar("test", {"join": join, "meet": meet, "mult": mult,
...     "over": const, "undr": const})
Traceback (most recent call last):
 ...
ValueError: multiplication must be distributive over join
>>> mult["0"]["0"] = "0"
>>> const["0"]["0"] = "0"
>>> ResiduatedBinar("test", {"join": join, "meet": meet, "mult": mult,
...     "over": const, "undr": const})
Traceback (most recent call last):
 ...
ValueError: check residuated binars axioms!
>>> mult = {"0": {"0": "0", "1": "0"}, "1": {"0": "1", "1": "1"}}
>>> undr = {"0": {"0": "1", "1": "1"}, "1": {"0": "0", "1": "1"}}
>>> ResiduatedBinar("test", {"join": join, "meet": meet, "mult": mult,
...     "over": mult, "undr": undr})
Traceback (most recent call last):
 ...
ValueError: check residuated binars axioms!
>>> print(binar.mace4_format[:10])
0 v 0 = 0.
check_axioms() → None

Check axioms specific to that algebraic structure.

If any axiom fails, raise an error.

property latex_mult_table: str

Return a LaTeX representation of a multiplication table.

property markdown_mult_table: str

Return a Markdown representation of a multiplication table.

property operation_map: Dict[str, str]

Return a map from operation labels to operation symbols.

Labels are used for the infix notation and symbols —

for functional one.

Abelian Group

class residuated_binars.abelian_group.AbelianGroup(label: str, operations: Dict[str, Dict[str, Any]])

An Abelian group structure.

>>> add = {"0": {"0": "0"}}
>>> group = AbelianGroup("test", {"add": add, "neg": {"0": "0"}})
>>> print(group.mace4_format)
0 + 0 = 0.
neg(0) = 0.
check_axioms() → None

Check axioms specific to that algebraic structure.

If any axiom fails, raise an error.

property operation_map: Dict[str, str]

Return a map from operation labels to operation symbols.

Labels are used for the infix notation and symbols —

for functional one.

Boolean Ring

class residuated_binars.boolean_ring.BooleanRing(label: str, operations: Dict[str, Dict[str, Any]])

A Boolean ring structure.

>>> add = {"0": {"0": "0", "1": "1"}, "1": {"0": "1", "1": "0"}}
>>> neg = {"0": "0", "1": "1"}
>>> mult = {"0": {"0": "0", "1": "0"}, "1": {"0": "0", "1": "1"}}
>>> ring = BooleanRing("test", {"add": add, "neg": neg, "mult": mult})
>>> print(ring.mace4_format)
0 + 0 = 0.
0 + 1 = 1.
1 + 0 = 1.
1 + 1 = 0.
neg(0) = 0.
neg(1) = 1.
0 * 0 = 0.
0 * 1 = 0.
1 * 0 = 0.
1 * 1 = 1.
check_axioms() → None

Check axioms specific to that algebraic structure.

If any axiom fails, raise an error.

property operation_map: Dict[str, str]

Return a map from operation labels to operation symbols.

Labels are used for the infix notation and symbols —

for functional one.

Pseudo-weak-\(R_0\) Algebra

class residuated_binars.pseudo_weak_r0_algebra.PseudoWeakR0Algebra(label: str, operations: Dict[str, Dict[str, Any]])

A representation of a peudo-weak-\(R_0\) algebra.

for more info look here

>>> join = {BOT: {BOT: BOT, TOP: TOP}, TOP: {BOT: TOP, TOP: TOP}}
>>> meet = {BOT: {BOT: BOT, TOP: BOT}, TOP: {BOT: BOT, TOP: TOP}}
>>> inv = {BOT: BOT, TOP: TOP}
>>> imp = {BOT: {BOT: TOP, TOP: TOP}, TOP: {BOT: BOT, TOP: TOP}}
>>> operations = {"imp1": imp, "imp2": imp, "inv1": inv, "inv2": inv,
...     "join": join, "meet": meet}
>>> PseudoWeakR0Algebra("no P1", operations)
Traceback (most recent call last):
 ...
ValueError: P1 axiom doesn't hold
>>> imp = {BOT: {BOT: TOP, TOP: TOP}, TOP: {BOT: TOP, TOP: TOP}}
>>> operations = {"imp1": imp, "imp2": imp, "inv1": inv, "inv2": inv,
...     "join": join, "meet": meet}
>>> PseudoWeakR0Algebra("no P1", operations)
Traceback (most recent call last):
 ...
ValueError: P2 axiom doesn't hold
check_axioms() → None

Check axioms specific to that algebraic structure.

If any axiom fails, raise an error.

Pseudo-\(R_0\) Algebra

class residuated_binars.pseudo_r0_algebra.PseudoR0Algebra(label: str, operations: Dict[str, Dict[str, Any]])

A representation of a peudo-\(R_0\) algebra.

for more info look here

>>> from residuated_binars.algebraic_structure import BOT
>>> imp = {
...     BOT: {BOT: TOP, TOP: TOP, "C3": TOP, "C2": TOP},
...     TOP: {BOT: BOT, TOP: TOP, "C3": "C3", "C2": "C2"},
...     "C3": {BOT: "C2", TOP: TOP, "C3": TOP, "C2": "C3"},
...     "C2": {BOT: "C3", TOP: TOP, "C3": TOP, "C2": TOP}
... }
>>> inv = {BOT: TOP, TOP: BOT, "C3": "C2", "C2": "C3"}
>>> join = {
...     BOT: {BOT: BOT, TOP: TOP, "C3": "C3", "C2": "C2"},
...     TOP: {BOT: TOP, TOP: TOP, "C3": TOP, "C2": TOP},
...     "C3": {BOT: "C3", TOP: TOP, "C3": "C3", "C2": "C3"},
...     "C2": {BOT: "C2", TOP: TOP, "C3": "C3", "C2": "C2"}
... }
>>> meet = {
...     BOT: {BOT: BOT, TOP: BOT, "C3": BOT, "C2": BOT},
...     TOP: {BOT: BOT, TOP: TOP, "C3": "C3", "C2": "C2"},
...     "C3": {BOT: BOT, TOP: "C3", "C3": "C3", "C2": "C2"},
...     "C2": {BOT: BOT, TOP: "C2", "C3": "C2", "C2": "C2"}
... }
>>> operations = {"imp1": imp, "imp2": imp, "inv1": inv, "inv2": inv,
...     "join": join, "meet": meet}
>>> PseudoR0Algebra("no P5", operations)
Traceback (most recent call last):
 ...
ValueError: P5 axiom doesn't hold
>>> imp = {
...     BOT: {BOT: TOP, TOP: TOP, "C3": TOP, "C2": TOP},
...     TOP: {BOT: BOT, TOP: TOP, "C3": "C3", "C2": "C2"},
...     "C2": {BOT: "C3", TOP: TOP, "C2": TOP, "C3": "C3"},
...     "C3": {BOT: "C2", TOP: TOP, "C2": "C2", "C3": TOP}
... }
>>> operations = {"imp1": imp, "imp2": imp, "inv1": inv, "inv2": inv,
...     "join": join, "meet": meet}
>>> PseudoR0Algebra("no P5", operations)
Traceback (most recent call last):
 ...
ValueError: P4 axiom doesn't hold
>>> imp = {
...     BOT: {BOT: TOP, TOP: TOP, "C3": TOP, "C2": TOP},
...     TOP: {BOT: BOT, TOP: TOP, "C3": "C3", "C2": "C2"},
...     "C2": {BOT: "C2", TOP: TOP, "C2": TOP, "C3": TOP},
...     "C3": {BOT: "C3", TOP: TOP, "C2": TOP, "C3": TOP}
... }
>>> inv = {BOT: TOP, TOP: BOT, "C3": "C3", "C2": "C2"}
>>> operations = {"imp1": imp, "imp2": imp, "inv1": inv, "inv2": inv,
...     "join": join, "meet": meet}
>>> PseudoR0Algebra("no P5", operations)
Traceback (most recent call last):
 ...
ValueError: P3 axiom doesn't hold
check_axioms() → None

Check axioms specific to that algebraic structure.

If any axiom fails, raise an error.

Using Isabelle to Generate Algebraic Structures

Constants

Generate Theories

This script creates a folder with a specified name and fills it with valid Isabelle theory files. Each theory file contains only one lemma without a proof and does not depend on any other theories. The exact statement of lemmas is hard-coded. It may have the following assumptions:

  • lattice axioms

  • residuation axioms

  • existence of the latest and the greatest elements of the lattice (they always exist in finite models)

  • a definition of the involution operation

  • some combination of abstract distributivity laws (from ASSUMPTIONS variable of constants.py)

The consequent of the lemma is one of the laws from ASSUMPTIONS which is not in the antecedent. So, if one has six laws in ASSUMPTIONS list, there will be 6 * (2 ^ 5 - 1) = 186 original hypotheses to check for models of different cardinalities.

The theory files are called T[number].thy where number enumerates theory files starting from zero.

residuated_binars.generate_theories.generate_isabelle_theory_file(theory_name: str, assumptions: List[str], goal: Optional[str] = None) → List[str]

Generate a text of Isabelle theory file with only ones lemma inside.

Parameters

  • theory_name – name of a theory file

  • assumptions – a list of lemma assumptions in Isabelle language

  • goal – the lemma goal in Isabelle language

Returns

a list of lines of a theory file

residuated_binars.generate_theories.independence_case(path: str, independent_assumptions: List[str], assumption_indices: List[int], goal_index: int, additional_assumptions: List[str]) → None

Generate theory of independence of an assumption from a subset of the rest.

Parameters

  • path – a folder for storing theory files

  • independent_assumptions – a list of assumption which independence we want to check

  • assumption_indices – indices of assumption to use

  • goal_index – index of a goal to prove

  • additional_assumptions – a list of additional assumptions about the binars like the lattice reduct distributivity, existence of an involution operation, and multiplication associativity

residuated_binars.generate_theories.independence_check(path: str, independent_assumptions: List[str], additional_assumptions: List[str], check_subset_independence: bool) → None

Generate a theory files to check independence given additional assumptions.

Parameters

  • path – a folder for storing theory files

  • independent_assumptions – a list of assumption which independence we want to check

  • additional_assumptions – a list of additional assumptions

  • check_subset_independence – whether to check every assumption from the list against all the rest or against any combination of the rest

Script for adding a task

  • for every theory file in a given folder

  • creates a new file with the same name in another given folder

  • the output file includes the same one lemma as the input

  • but the ‘task’ is changed according to the script’s parameters

Possible task types:

  • TaskType.NITPICK, demands a cardinality to be provided as well (finite model search)

  • TaskType.SLEDGEHAMMER (automated proof search)

Both task types have a hard-coded timeout of 1000000 seconds.

class residuated_binars.add_task.TaskType(value)

Type of tasks to ask isabelle server to perform.

residuated_binars.add_task.add_task(source_path: str, target_path: str, task_type: TaskType, cardinality: int = 1) → None

Take theory files from an existing folder and change tasks in them.

Parameters

  • source_path – a directory where to get theory files to add tasks to

  • target_path – where to put new theory files with added tasks

  • task_type – use Nitpick or Sledgehammer (disprove by finding a finite counter-example or prove)

  • cardinality – a cardinality of finite model to find (only for Nitpick tasks)

Check Assumptions

  • gets all theory files from a given directory

  • constructs a command for Isabelle server to process these files

  • saves the log of Isabelle server replies to the file named isabelle.out in the directory where the theory files are

This script depends on Python client for Isabelle server.

residuated_binars.check_assumptions.check_assumptions(path: str, server_info: Optional[str] = None) → None

Ask Isabelle server to process all theory files in a given path.

Parameters

  • path – a folder with theory files

  • server_info – an info string of an Isabelle server

residuated_binars.check_assumptions.get_abs_path(path: str) → str

Get an absolute path on Windows or Linux.

Parameters

path – a path

Returns

an absolute path, corrected to CygWin path for Windows

residuated_binars.check_assumptions.get_customised_logger(task_folder: str) → Logger

Get a nice logger.

Parameters

task_folder – a base folder (and a task name)

Filter Theories

  • reads from isabelle.out file from the input directory (this directory should be an output of check_assumption.py script)

  • filters only those theory files, for which neither finite model was found, nor the proof (depending on the task type)

  • copies filtered theory files from the input directory to another given directory

residuated_binars.filter_theories.filter_theories(source_path: str, target_path: str) → None

Filter theories which don’t have neither counter-example nor a proof yet.

Get theory files from an existing folder and copy to another existing folder ones those of them, for which neither have a finite counter-example nor a proof.

Parameters

  • source_path – where to look for processed theory files; should include an isabelle.out file with server’s output

  • target_path – where to put theory files without proofs or counter-examples

Raises

ValueError – if there is no FINISHED message in Isabelle server response

Use Nitpick

A wrapper ‘do all’ script.

  • runs generate_theories.py which creates a new hyp2 folder with initial hypotheses templates

  • then for each cardinality from 2 to 100 (hard-coded)

  • runs add_task.py which creates a task[n] folder for a particular cardinality with a respective task for Nitpick added to the templates in hyp[n]

  • runs check_assumptions.py on a task[n] folder

  • runs filter_theories.py which filter theories with no counter-examples found to a new folder hyp[n+1]

  • if the hyp[n+1] folder is empty, the script stops (that means counter-examples were found for all original hypotheses)

residuated_binars.use_nitpick.use_nitpick(max_cardinality: int, independent_assumptions: List[str], additional_assumptions: List[str], check_subset_independence: bool, server_info: Optional[str] = None) → None

Incrementally search for finite counter-examples.

Parameters

  • max_cardinality – maximal cardinality of a model to search for

  • independent_assumptions – a list of assumption which independence we want to check

  • additional_assumptions – a list of additional assumptions

  • check_subset_independence – whether to check every assumption from the list against all the rest or against any combination of the rest

  • server_info – an info string of an Isabelle server

Short scripts useful for other sub-modules

residuated_binars.utils.remove_dirs(dir_list: Sequence[str]) → None

Remove a list of sub-directories of a current one.

>>> os.path.exists("remove-test1")
False
>>> os.path.exists("remove-test2")
False
>>> os.mkdir("remove-test1")
>>> os.mkdir(os.path.join("remove-test1", "some"))
>>> os.mkdir("remove-test2")
>>> os.path.exists(os.path.join("remove-test1", "some"))
True
>>> os.path.exists("remove-test2")
True
>>> remove_dirs(("remove-test*",))
>>> os.path.exists("remove-test1")
False
>>> os.path.exists("remove-test2")
False
Parameters

dir_list – sub-folders of the current folder to remove completely (no questions asked!)