Formula¶

class logics.classes.propositional.Formula(*args, **kwargs)¶

Class for representing propositional formulae.

The class Formula extends list. Every subformula within a Formula must also be a Formula.

Atomic formulae contain a single string element, e.g. Formula(['p']); Formula(['A']); Formula(['⊥'])

Molecular formulae are always written in prefix notation, e.g. Formula(['∧', ['p'], ['~', ['q']]]), which is read as p ∧ ~q

Note that the __init__ method of Formula will automatically turn lists within a Formula into Formula. Thus, you can write Formula(['~', ['p']]) instead of Formula(['~', Formula(['p'])])

Examples

>>> from logics.classes.propositional import Formula
>>> f = Formula(['~', ['p']])
>>> f[1]
['p']
>>> type(f[1])
<class 'logics.classes.propositional.formula.Formula'>

Notes

Working with Formula elements directly is somewhat uncomfortable and cumbersome. You may instead want to take a look at Parsers. For random generation of formulae, see Random Formula Generators

property is_atomic¶

Returns True if the formula is atomic.

Will consider a formula as an atomic if it is of length 1 (so as to not have to pass a Language as parameter).

Examples

>>> from logics.classes.propositional import Formula
>>> Formula(['p']).is_atomic
True
>>> Formula(['~', ['p']]).is_atomic
False

arguments(quantifiers=None)¶

Returns a list of the arguments of a molecular formula, [] if it is an atomic.

Examples

>>> from logics.classes.propositional import Formula
>>> Formula(['p']).arguments()
[]
>>> Formula(['∧', ['p'], ['~', ['A']]]).arguments()
[['p'], ['~', ['A']]]

Notes

quantifiers parameter is necessary because of how PredicateFormula works. Leave it as None here.

is_schematic(language)¶

Returns True if the formula contains a metavariable of the language, False otherwise

Examples

>>> from logics.classes.propositional import Formula
>>> from logics.instances.propositional.languages import classical_language
>>> Formula(['p']).is_schematic(classical_language)
False
>>> Formula(['A']).is_schematic(classical_language)
True
>>> Formula(['∧', ['p'], ['~', ['A']]]).is_schematic(classical_language)
True

property main_symbol¶

Returns the first element if the formula is molecular, None if it is an atomic.

Examples

>>> from logics.classes.propositional import Formula
>>> Formula(['p']).main_symbol is None
True
>>> Formula(['∧', ['p'], ['~', ['A']]]).main_symbol
'∧'

property depth¶

Depth of the formula.

Examples

>>> from logics.classes.propositional import Formula
>>> Formula(['p']).depth
0
>>> Formula(['∧', ['p'], ['~', ['A']]]).depth
2

is_well_formed(language)¶: Shortcut for language.is_well_formed(formula)

property subformulae¶

Returns a list of the subformulae of the formula, without repetitions.

Examples

>>> from logics.classes.propositional import Formula
>>> Formula(['p']).subformulae
[['p']]
>>> Formula(['∧', ['p'], ['~', ['A']]]).subformulae
[['p'], ['A'], ['~', ['A']], ['∧', ['p'], ['~', ['A']]]]
>>> Formula(["∧", ["p"], ["p"]]).subformulae  # p will only appear once
[['p'], ['∧', ['p'], ['p']]]

atomics_inside(language, prev_at=None)¶

Returns the set of the atomic letter strings (both propositional letters and metavariables) inside a formula. Sentential constants do not count.

Examples

>>> from logics.classes.propositional import Formula
>>> from logics.instances.propositional.languages import classical_language
>>> Formula(['∧', ['p'], ['~', ['A']]]).atomics_inside(classical_language)
{'A', 'p'}

substitute(sf_to_substitute, sf_with)¶

Substitutes a subformula for another subformula.

Will return a different Formula object, and not modify the original.

The substituted one must match exactly, for example, calling Formula(['∧', ['p'], ['B']]).substitute with arguments sf_to_substitute=Formula(['∧', ['A'], ['B']]) and sf_with=Formula(['∧', ['B'], ['B']] will do nothing. See below for a different method that will do something with that. This method is also different from the PredicateFormula free variable substitution method.

Parameters:

sf_to_substitute (logics.classes.propositional.Formula) – The subformula you wish to substitute
sf_with (logics.classes.propositional.Formula) – The subformula you wish to substitute it with

Returns:

A different formula instance from the original

Return type:

logics.classes.propositional.Formula

Examples

>>> from logics.classes.propositional import Formula
>>> f = Formula(['∧', ['p'], ['~', ['A']]])
>>> f.substitute(Formula(['~', ['A']]), Formula(['~', ['p']]))
['∧', ['p'], ['~', ['p']]]
>>> f
['∧', ['p'], ['~', ['A']]]

instantiate(language, subst_dict)¶

Given a schematic Formula, a language and a substitution dict, returns the schema instantiated with the dict.

Will return a different Formula object, and not modify the original.

Parameters:

language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
subst_dict (dict) – The susbstitution dict must have form {'A': someformula, 'B': someformula}

Returns:

A different formula instance from the original

Return type:

logics.classes.propositional.Formula

Raises:

ValueError – if some schematic propositional within the formula has no substitution assigned in the dictionary

Examples

>>> from logics.classes.propositional import Formula
>>> from logics.instances.propositional.languages import classical_language
>>> f = Formula(['∧', ['A'], ['B']])
>>> f.instantiate(classical_language, {'A': Formula(['B']),
...                                    'B': Formula(['∧', ['~', ['B']], ['C']])})
['∧', ['B'], ['∧', ['~', ['B']], ['C']]]
>>> f
['∧', ['A'], ['B']]
>>> Formula(['∧', ['A'], ['B']]).instantiate(classical_language, {'A': Formula(['p'])})
Traceback (most recent call last):
...
ValueError: Metavariable B not present in substitution dict given

schematic_substitute(language, schema_to_substitute, schema_with)¶

Takes a Formula and two schematic Formula, and substitutes any subformula instance of the first schema for the corresponding instance of the second schema.

Will return a different Formula object, and not modify the original.

Parameters:

language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
schema_to_substitute (logics.classes.propositional.Formula) – The schema of the subformula you wish to substitute
schema_with (logics.classes.propositional.Formula) – The schema of the subformula you wish to substitute it with

Returns:

A different formula instance from the original

Return type:

logics.classes.propositional.Formula

Examples

>>> from logics.classes.propositional import Formula
>>> from logics.instances.propositional.languages import classical_language
>>> f = Formula(['→', ['p'], ['→', ['p'], ['q']]])
>>> f.schematic_substitute(classical_language, Formula(['→', ['A'], ['B']]),
...                                            Formula(['∨', ['~', ['A']], ['B']]))
['∨', ['~', ['p']], ['∨', ['~', ['p']], ['q']]]
>>> f
['→', ['p'], ['→', ['p'], ['q']]]

is_instance_of(formula, language, subst_dict=None, return_subst_dict=False, order=None)¶

Determines if a Formula is an instance of another (tipically schematic) Formula.

For two non-schematic formulae, one is considered an instance of another iff they are equal.

Has two optional parameters:

return_subst_dict: defaults to False. If True, will return the substitution dict for formula’s metavariables. See below for an example.

subst_dict: defaults to None. Can be given a substitution dict if some metavariable(s) are to be interpreted in some specific way.

These parameters are useful in other modules, e.g. for checking correct instantiation of rules, where you tipically first check the conclusion, return a susbstitution dict, and use that substitution dict to check the premises of the rule. See below for some examples.

Parameters:

formula (logics.classes.propositional.Formula) – The (schematic) Formula of which we want to know if it is instance
language (logics.classes.propositional.Language or logics.classes.propositional.InfiniteLanguage) – Instance of Language or InfiniteLanguage
subst_dict (dict, optional) – A susbstitution dict of the form {'A': someformula, 'B': someformula}
return_subst_dict (bool, optional) – If True will additionally return a substitution dict.
order (NoneType, optional) – Is for the is_instance_of method of Inference. Does nothing here, you should not alter it.

Examples

>>> from logics.classes.propositional import Formula
>>> from logics.instances.propositional.languages import classical_language
>>> Formula(['~', ['p']]).is_instance_of(Formula(['A']), classical_language)
True
>>> Formula(['~', ['p']]).is_instance_of(Formula(['∨', ['A'], ['B']]), classical_language)
False
>>> Formula(['∨', ['~', ['p']], ['q']]).is_instance_of(Formula(['∨', ['A'], ['B']]),
...                                                    classical_language)
True

If we give it some substitution dict beforehand:

>>> Formula(['p']).is_instance_of(Formula(['A']), classical_language,
...                               subst_dict={'A': Formula(['q'])})
False
>>> Formula(['p']).is_instance_of(Formula(['A']), classical_language,
...                               subst_dict={'A': Formula(['p'])})
True

If we ask it to return the substitution dict:

>>> Formula(['∨', ['~', ['p']], ['q']]).is_instance_of(Formula(['∨', ['A'], ['B']]),
...                                                    classical_language,
...                                                    return_subst_dict=True)
(True, {'A': ['~', ['p']], 'B': ['q']})