New answers tagged logic
1
The relationship between the two is related to intuistionistic logic vs. classical logic. When you add sufficiently powerful versions of the excluded middle law to Curry-Howard-style type systems, you can translate between propositions (types of sort Prop, which are inhabited if and only if they are provable) and Boolean values at will. Check out the list of ...
1
Does it mean that a logic system is a programming language, where types are propositions and values of a type are proofs of the proposition?
Not necessarily, being both (logic systems and programming language) formal languages, there certainly is a certain degree of isomorphism between the two concepts, this translates into the fact that we can encode a ...
2
I think you are really asking a question about the definition of the notion of well-foundedness.
I think the notion of loop variants is a bit of a red herring here: I would argue that any reasonable definition of well-foundedness should enable proving that a loop is terminating iff there is a well-founded relation which acts as a variant for it, almost as a ...
2
It is equivalent to
$$\bigwedge_{k=1}^{N} \bigvee_{i_k=1}^{M} x_{i_k k}.$$
This is a much simpler expression: $NM$ terms instead of $M^N$ terms, if you expand everything out.
0
If the current state is one of $a,b$, then the following state is one of $b,c$.
2
As you correctly point out, the original formula is valid (in every model either there is some element for which p or q doesn't hold, or p and q hold for all elements).
To prove that your formula is valid, you cannot use resolution directly. Recall that with resolution, you can derive the empty clause from a clause set iff the clause set is unsatisfiable. ...
3
Regular expressions are at the very core of computer science, conceptually and historically.
Kleene's article in which he introduced them and proved them equal in power to finite automata is one of the foundational articles of computer science. It was the foundation of formal language theory, which was based on its results and its approach; it is an ...
1
Honestly, I don't think the "discovered" vs "invented" is a distinction that matters. If you want to get into that, fine, but it's a matter of philosophy, not science.
To your main point, yes, regular languages are very much a part of computer science because, regardless of their history, they identify a class of computational problems and correspond to a ...
7
There are several things that are all called regular expressions. The answer to your question is different depending upon which thing you want to talk about.
The three relevant distinctions for this question in my opinion are as follows:
First
The notion of regular languages and related things like recursive enumerability.
Individual regular languages ...
1
I'm fairly sure this is possible. This seems to me as a special case of set constraints over tree languages: we can view regular expressions as a restriction of regular tree languages where each node has 0 or 1 children. These can handle union, concatenation, and recursion (star), and you can solve for variables like you describe.
They're decidable, even ...
Top 50 recent answers are included
