Random Formula Generators¶

class logics.utils.formula_generators.generators_biased.BiasedPropositionalGenerator¶

A biased random propositional generator.

It is biased because it will not return every formula/inference within the space asked with the same probability. On the other hand, it is much faster than its non-biased counterpart.

Examples

This generator takes no parameters, so to instantiate one you can simply do:

>>> from logics.utils.formula_generators.generators_biased import BiasedPropositionalGenerator
>>> random_generator = BiasedPropositionalGenerator()

There is also a predefined instance so there is even no need to instantiate it

>>> from logics.utils.formula_generators.generators_biased import random_formula_generator

random_formula(depth, atomics, language, exact_depth=True, all_atomics=False)¶

Generates a random formula for the language given.

Parameters

depth (int) – A positive integer, representing the depth of the formula to obtain
atomics (list of str) – The sublist of atomics of the language that the formula will be built of
language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
exact_depth (bool) – If true, the resulting formula will have exactly the depth given. Otherwise, will have up to that depth. Defaults to True.
all_atomics (bool) – If true, the resulting formula will contain all the atomics given. Otherwise, can contain some of them. Defaults to False.

Returns

A randomly generated formula of the given depth, containing some or all the atomics

Return type

logics.classes.propositional.Formula

Raises

NotImplemented – If exact_depth is False and all_atomics is True
ValueError – If exact_depth is True, all_atomics is True and the number of atomics given > the maximum arity constant of the language ** depth. For example, it is not possible to build a formula of depth 1 with 3 atomics in a language that has connectives of at most arity 2.

Examples

Exact depth and not all atomics

>>> from logics.instances.propositional.languages import classical_language
>>> from logics.utils.formula_generators.generators_biased import random_formula_generator
>>> random_formula_generator.random_formula(depth=3, atomics=['p', 'q', 'r'],
...                                         language=classical_language,
...                                         exact_depth=True, all_atomics=False)
['→', ['→', ['p'], ['↔', ['r'], ['p']]], ['~', ['r']]]
>>> random_formula_generator.random_formula(depth=3, atomics=['p', 'q', 'r'],
...                                         language=classical_language,
...                                         exact_depth=True, all_atomics=False)
['↔', ['∨', ['~', ['r']], ['r']], ['↔', ['p'], ['q']]]

Not exact depth and not all atomics

>>> random_formula_generator.random_formula(depth=3, atomics=['p', 'q', 'r'],
...                                         language=classical_language,
...                                         exact_depth=False, all_atomics=False)
['∨', ['r'], ['q']]
>>> random_formula_generator.random_formula(depth=3, atomics=['p', 'q', 'r'],
...                                         language=classical_language,
...                                         exact_depth=False, all_atomics=False)
['→', ['r'], ['∨', ['p'], ['r']]]

Exact depth and all atomics

>>> random_formula_generator.random_formula(depth=3, atomics=['p', 'q', 'r'],
...                                         language=classical_language,
...                                         exact_depth=True, all_atomics=True)
['~', ['∧', ['∧', ['r'], ['q']], ['p']]]
>>> random_formula_generator.random_formula(depth=3, atomics=['p', 'q', 'r'],
...                                         language=classical_language,
...                                         exact_depth=True, all_atomics=True)
['∨', ['∨', ['∧', ['q'], ['r']], ['→', ['r'], ['q']]], ['p']]

random_inference(num_premises, num_conclusions, max_depth, atomics, language, level=1, exact_num_premises=True, exact_num_conclusions=True)¶

Generates a random Inference.

Takes a number of premises and of conclusions (either exact or up to, see the exact_num_premises and exact_num_conclusions parameters below), and populates them with formuale of up to the given max_depth and some of the given atomics.

Can also be used to generate metainferences, if given a level > 1. In that case, the inferences in the premises / conclusions will have up to that number of premises and conclusions. That is, if asked for an inference of level 2 with exactly two premises, the premises will themselves be inferences, and they may contain less than two premises.

Parameters

num_premises (int) – The exact number of premises the inference will contain
num_conclusions (int) – The exact number of conclusions the inference will contain
max_depth (int) – The maximum depth that the formulae within the inference can contain
atomics (list of str) – The sublist of atomics of the language that the formulae within the inference will be built of
language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
level (int, optional) – Level of the inference to be generated (1 is regular inference, 2 is metainference, 3 is metameta, …). level is 1 by default.
exact_num_premises (bool) – If True, the resulting inference will contain will contain exactly that number of premises, otherwise will contain up to that number of premises. Defaults to True.
exact_num_conclusions (bool) – If True, the resulting inference will contain will contain exactly that number of premises, otherwise will contain up to that number of premises. Defaults to True.

Returns

A randomly generated inference of the given parameters.

Return type

logics.classes.propositional.Inference

Examples

Random inferences with exactly two premises and one conclusion:

>>> from logics.instances.propositional.languages import classical_language
>>> from logics.utils.parsers import classical_parser
>>> from logics.utils.formula_generators.generators_biased import random_formula_generator
>>> inf = random_formula_generator.random_inference(num_premises=2, num_conclusions=1,
...                                                 max_depth=2, atomics=['p', 'q'],
...                                                 language=classical_language, level=1,
...                                                 exact_num_premises=True,
...                                                 exact_num_conclusions=True)
>>> classical_parser.unparse(inf)
'(p ∧ p), ((q ∨ q) ∧ (p ∨ p)) / ~q'
>>> inf = random_formula_generator.random_inference(num_premises=2, num_conclusions=1,
...                                                 max_depth=2, atomics=['p', 'q'],
...                                                 language=classical_language, level=1,
...                                                 exact_num_premises=True,
...                                                 exact_num_conclusions=True)
>>> classical_parser.unparse(inf)
'~(q ↔ q), q / (q ∧ (p → p))'

Random inferences with up to two premises and two conclusions

>>> inf = random_formula_generator.random_inference(num_premises=2, num_conclusions=2,
...                                                 max_depth=2, atomics=['p', 'q'],
...                                                 language=classical_language, level=1,
...                                                 exact_num_premises=False,
...                                                 exact_num_conclusions=False)
>>> classical_parser.unparse(inf)
'(p ↔ p) / ~q'
>>> inf = random_formula_generator.random_inference(num_premises=2, num_conclusions=2,
...                                                 max_depth=2, atomics=['p', 'q'],
...                                                 language=classical_language, level=1,
...                                                 exact_num_premises=False,
...                                                 exact_num_conclusions=False)
>>> classical_parser.unparse(inf)
'/'

Random metainferences with up to two premises and two conclusions

>>> inf = random_formula_generator.random_inference(num_premises=2, num_conclusions=2,
...                                                 max_depth=2, atomics=['p', 'q'],
...                                                 language=classical_language, level=2,
...                                                 exact_num_premises=False,
...                                                 exact_num_conclusions=False)
>>> classical_parser.unparse(inf)
'((q → (q → q)) /), ((p ↔ p), (q ∧ p) / (q ∨ q), p) //'
>>> inf = random_formula_generator.random_inference(num_premises=2, num_conclusions=2,
...                                                 max_depth=2, atomics=['p', 'q'],
...                                                 language=classical_language, level=2,
...                                                 exact_num_premises=False,
...                                                 exact_num_conclusions=False)
>>> classical_parser.unparse(inf)
'(/) //'

random_tautology(depth, atomics, language, validity_apparatus, exact_depth=True, all_atomics=False, attempts=100)¶

Generates a random tautogy for the validity apparatus given.

Will generate a random formula and then test the inference ([] / [formula]) to see if it is valid. If it is, returns it, otherwise generates another. Can fail for at most the number of attempts given.

The signature is very similar to that of random_formula but takes two extra parameters:

validity_apparatus: any object with an is_valid method (which takes an inference as argument)

attempts: an int, maximum number of formulae it generates and tests (defaults to 100)

Returns

A randomly generated tautology of the given depth, containing some or all the atomics

Return type

logics.classes.propositional.Formula

Raises

NotImplemented – If exact_depth is False and all_atomics is True
ValueError – If exact_depth is True, all_atomics is True and the number of atomics given > the maximum arity constant of the language ** depth.
FormulaGeneratorError – If it cannot find a tautology in the given number of attempts

Examples

>>> from logics.instances.propositional.languages import classical_language
>>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics
>>> from logics.utils.formula_generators.generators_biased import random_formula_generator
>>> random_formula_generator.random_tautology(depth=2, atomics=['p', 'q'],
...                                           language=classical_language,
...                                           validity_apparatus=classical_mvl_semantics)
['→', ['∧', ['q'], ['p']], ['∧', ['q'], ['q']]]
>>> random_formula_generator.random_tautology(depth=2, atomics=['p', 'q'],
...                                           language=classical_language,
...                                           validity_apparatus=classical_mvl_semantics)
['→', ['p'], ['∨', ['p'], ['p']]]

random_valid_inference(num_premises, num_conclusions, max_depth, atomics, language, validity_apparatus, level=1, exact_num_premises=True, exact_num_conclusions=True, attempts=100)¶

Generates a random valid inference for the validity apparatus given.

Similar to the random_inference method. The two new parameters are to the method above. In particular, The object passed to validity_apparatus must have an is_valid method. If level > 1 the validity apparatus must be able to handle metainferential validity.

Returns: A randomly generated valid inference or metainference with the parameters given
Return type: logics.classes.propositional.Inference
Raises: FormulaGeneratorError – If it cannot find a valid inference in the given number of attempts

Examples

>>> from logics.instances.propositional.languages import classical_language
>>> from logics.utils.parsers import classical_parser
>>> from logics.instances.propositional.many_valued_semantics import classical_mvl_semantics
>>> from logics.utils.formula_generators.generators_biased import random_formula_generator
>>> inf = random_formula_generator.random_valid_inference(num_premises=2, num_conclusions=1,
...                                                       max_depth=2, atomics=['p', 'q'],
...                                                       language=classical_language, level=1,
...                                                       validity_apparatus=classical_mvl_semantics)
>>> classical_parser.unparse(inf)
'(q ↔ p), p / (p ∨ q)'
>>> inf = random_formula_generator.random_valid_inference(num_premises=2, num_conclusions=1,
...                                                       max_depth=2, atomics=['p', 'q'],
...                                                       language=classical_language, level=2,
...                                                       validity_apparatus=classical_mvl_semantics)
>>> classical_parser.unparse(inf)
'(p / p), (p, ((q → p) ∧ (p ∨ p)) / (p ↔ (q ↔ p))) // (((p ↔ p) ∨ p), ~q / (q ∨ ~p))'

random_invalid_inference(num_premises, num_conclusions, max_depth, atomics, language, validity_apparatus, level=1, exact_num_premises=True, exact_num_conclusions=True, attempts=100)¶

Generates a random invalid inference for the validity apparatus given.

Identical to the method above, only that it returns an invalid inference.