Zulip Chat Archive

Stream: new members

Topic: Complexity of a propositional formula


view this post on Zulip Donald Sebastian Leung (Feb 22 2020 at 05:17):

In the Chapter 7 exercises in "Theorem Proving in Lean", question 4 asks me to define the type of propositional formulas and a function for measuring the complexity of a formula, among other things. What is meant by "complexity of a formula" here?

view this post on Zulip Floris van Doorn (Feb 22 2020 at 07:15):

Usually it means something like the length of a formula, the number of variables plus the number of logical symbols (like connectives/negations). But it could mean different things, like the depth (how many nested logical connectives are there).

view this post on Zulip Donald Sebastian Leung (Feb 22 2020 at 07:16):

I see, thanks. So there's no universally accepted definition of "complexity of a formula"?

view this post on Zulip Floris van Doorn (Feb 22 2020 at 07:21):

I don't think so, but if there was I would guess the number of symbols in it.

view this post on Zulip Floris van Doorn (Feb 22 2020 at 07:23):

For first-order logic formulas there is a different kind of complexity, which counts the number of quantifier changes (in a certain normal form): https://en.wikipedia.org/wiki/Arithmetical_hierarchy
But this doesn't make sense for propositional formulae, since there are no quantifiers.

view this post on Zulip Marc Huisinga (Feb 22 2020 at 08:11):

my guess is that it's asking for some kind of evaluation complexity (i.e. how many steps it would take to evaluate the formula), given that it also asks to implement evaluation right before that

view this post on Zulip Mario Carneiro (Feb 22 2020 at 08:27):

Generally when this term is used it doesn't really matter what it is precisely, as long as it's a natural number and subformulas have smaller complexity

view this post on Zulip Mario Carneiro (Feb 22 2020 at 08:29):

quantifier alternations is usually called "arithmetic complexity" specifically


Last updated: May 11 2021 at 00:31 UTC