This function takes putdown notation for one or more LogicConcepts and builds instances of them by parsing the input, returning an array of the results. Putdown is a simple format, and so it plays on the name of the famous simple format "markdown," but turns it into something that sounds undesirable (and humorous?). Putdown and Markdown have no connection, neither historically nor in the format itself.

Putdown notation is defined as follows.

• A Symbol is written using any sequence of non-whitespace characters that does not include or conflict with the special characters below. Thus symbols are quite flexible, including things like x and y as well as -459.7001 and $===_-_@_-_===$ and much more.
• A Symbol can also be written as a string literal whose only escape characters are \" inside double-quoted literals, \' inside single-quoted literals, and \n or \\ in any case. Thus you can create just about any symbol at all, including "{ yes it's (a symbol) }", which is not a compound expression, but is a single atomic symbol.
• An Application is written using LISP notation. Function application requires at least one argument (no empty paren pairs). For example, you might write $\sin x$ as (sin x).
• A BindingExpression is written as a series of Symbols, separated by commas, followed by another comma, and then the body expression. All children before the body and after the first child must be Symbols, and are the bound variables. Example: x , (P x) means $P(x)$ with $x$ bound. Consequently, could write, for example, (∀ x , (P x)) to mean the application of the ∀ symbol to the binding x , (P x).
• A Declaration lists the declared Symbols in brackets, followed optionally by a comma and then a body, which is any LogicConcept. that is an assumption made about the variables. Example: [x , (P x)] means "Declare $x$ about which $P(x)$ is true." This can be used for arbitrary variables (in which we would be assuming $P(x)$) or declaring constants we know to exist (in which we would be concluding $P(x)$) or for anything else the user's library wants to use declarations for.
• An Environment is written with its children separated by spaces and surrounded in curly brackets. Example: { child1 child2 etc }.
• Any Environment, Declaration, or outermost Expression can be marked as a "given" by preceding it with a colon, :.
• Any Environment, Declaration, or Expression can be given additional attributes by following it with +{ and then for the rest of the line (that is, until the next newline) writing as much JSON code as you like, beginning with that initial {, as attributes to add to the preceding object. For example, to add the color green to a Symbol, we might do this: my_symbol +{"color":"green"}. To add more attributes than can fit on one line, simply start another +{...} block on the next line.
• The notation // is used for one-line comments. Anything after it is ignored, up until the next newline. The previous rule has some conflict with this one, and we resolve it as follows. If a // occurs before a +{ on a line, then the // takes precedence and the rest of the line is a comment, so the +{ is ignored. But if the +{ appears first, it takes precedence, and the rest of the line is interpreted as JSON code, so a trailing // comment will most likely create invalid JSON, and thus should be avoided.

LogicConcepts can be thought of as expression a fragment of propositional logic if we view givens (that is, LogicConcepts satisfying .isA( 'given' )) as saying "if this is true..." and those that are not givens as saying "...then this is true." For example, we would view the LogicConcept expressed by the putdown notation { :{ A B } C D } as saying "if A and B are true then C and D are true," or in propositional logic notation as $(A\wedge B)\to(C\wedge D)$.

This function helps us express such propositional sentences using only conditionals, that is, not needing conjunctions. The above example would be written as two separate sentences, one saying "if A then if B then C" and another saying "if A then if B then D," or in propositional logic notation as the sentences $A\to B\to C$ and $A\to B\to D$, where the conditional arrow associates to the right. We interpret the set of such propositional expressions as meaning their conjunction. Thus there is one implied conjunction over all of the conditional expressions, and so this is a type of normal form.

It returns a list of LogicConcepts, each of which is either a single Expression, which should be interpreted as a single propositional letter, or an Environment whose only claim child is its last, that is, one of the form { :G_1 ... :G_n C }, containing $n$ givens and 1 claim.

The current version of this function supports only inputs containing nested Environments and Expressions, not inputs that may contain Declarations. Any Declarations are just ignored.

Enable or disable feedback, optionally flushing the queue of any old, stored feedback from when feedback was disabled.

To understand what it means for feedback to be enabled or disabled, see the documentation for feedback().

This method does one of two things, depending on whether feedback for this instance is enabled, which can be customized using enableFeedback().

If feedback is enabled and this object has an origin(), then this method just calls the feedback() method in that origin, with the same parameter. The reason for this is that feedback to the LDE about a LogicConcept should always be mediated through the MathConcept that gave rise to that LogicConcept.

If feedback is disabled, then the feedback given as the parameter will be stored in a feedback queue, which can be discarded or flushed later, using enableFeedback().

Note that there is no third option; if feedback is enabled, but this object has no origin(), then there is no way for this object to send the requested feedback, so this method will take no action.

Whether a LogicConcept has an ancestor chain that is all claims is often a crucial query. It is a large part of the definition of conclusions, for example, but can also be applied to Environments and other LogicConcepts.

This function returns true if this LogicConcept or any of its ancestors is marked as a given (using the isA() function), up to but not including the ancestor passed as the inThis parameter. If that parameter is omitted, all ancestors up to and including the topmost are searched, and if any is a given, this function returns false. Otherwise it returns true.

Overrides the behavior in the parent class, where the default behavior is to propagate dirtiness up to ancestors, whereas we do not want that here. The reason is that MathConcepts use the dirty flag to indicate whether they need to have their interpretation recomputed, but LogicConcepts use the dirty flag to indicate whether they need to have their validation recomputed. Interpretation tends to depend on the interpretation of children, whereas validation does not.

Many LogicConcept instances will be created by interpreting a MathConcept, and breaking it down into smaller, simpler parts, expressed as LogicConcepts. We will typically want to track, for any given LogicConcept, which MathConcept it came from, in that sense. This function returns that value.

There is no corresponding setter function, because it is not expected that clients should be changing the origin of a LogicConcept. Later, when we implement interpretation of MathConcepts into LogicConcepts, we will populate this value in that code.

This function is the inverse of fromPutdown(), which creates LogicConcept instances from text in putdown notation. This function writes putdown notation for any LogicConcept. It should be the case that this function outputs valid putdown notation for any LogicConcept in which it is called, and that fromPutdown() applied to that notation produces an object that equals() the original.