Random Formula Generators

class logics.utils.formula_generators.generators_biased.BiasedPredicateGenerator

A biased random predicate generator.

It is biased because it will not return every formula/inference within the space asked with the same probability. There is no non-biased generator implemented in this package yet. This implementation does not yet work with function symbols.

Examples

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

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

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

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

random_formula(depth, predicates, max_predicate_arity, ind_constants, variables, language, remaining_depth=0, predicate_arities=None)

Generates a random formula of some exact depth, which uses some of the predicates, variables and ind cts provided

Because of the educational usecases I have in mind, I don’t want it to output things like ∀x P(a) or like ∀x ∀x P(x). More precisely, Its made so every quantifier binds at least one variable.

Assumes that the predicate arities can be random (i.e. will not respect the predicate_letters={‘P’: 1, ‘Q’: 1, ‘R’: 2, ‘S’: 3} argument given to PredicateLanguage). If you want it to, give it predicate_arities=language.predicate_letters

Examples

>>> from logics.instances.predicate.languages import classical_predicate_language as lang
>>> from logics.utils.parsers import classical_predicate_parser
>>> from logics.utils.formula_generators.generators_biased import random_predicate_formula_generator
>>> for _ in range(5):
...     formula = random_predicate_formula_generator.random_formula(depth=2, predicates=['P', 'Q'],
...         max_predicate_arity=2, ind_constants=['a', 'b'], variables=['x', 'y'], language=lang)
...     print(classical_predicate_parser.unparse(formula))
Q(b, a) → ∀x Q(x, x)
∀y Q(y) ∧ Q(b)
∀x (Q(b) ∧ P(x, a))
∀y (Q(y, a) ∧ P(y, y))
∃x P(x) ∨ P(b)