Questions related to mathematical logic and its use in computer science

learn more… | top users | synonyms (1)

0
votes
1answer
31 views

Difference between equivalence and implication

In terms of CTL formulae, what is the difference between equivalence and implication? (prop = some proposition, && = conjunction, AG = CTL syntax for "globally holds") E.g. AG (prop1 ...
1
vote
1answer
30 views

How can I translate this quantified logical expression into english

I was reading chapter-1 The Foundations: Logic and Proofs from this book. The chapter gives example of translating English sentence : "There is a woman who has taken a flight on every airline in the ...
-1
votes
1answer
30 views

Meaning of empty clause

Why does the empty clause is logically equivalent to a contraddiction: $\square \cup \square \Longleftrightarrow \perp$ and why the empty cube is logically equivalent to a tautology: $\square \cap ...
2
votes
1answer
22 views

Terminology about the word Function : General vs Computable

I've seen two different concepts referred to by the term "function": A small part of a program specified by the composition of constants and other functions as paramaters, such as the "functions" in ...
1
vote
2answers
30 views

Using the rules of inferences

I know the rules of inferences and logical equivalence but I cannot seem to validate this argument. I rewrote the first premise as $\neg p\vee q$ other from that I am stuck. Any help will be ...
2
votes
1answer
65 views

Computational equivalences between a calculus and an automaton model

This Wikipedia table (template for "Formal languages and grammars") maps grammar to language to abstract machine for more than a dozen languages. ...
0
votes
2answers
47 views

How can I simplify the following Product of Sums: ab+ac'+a'b'+a'c+b'c'+bc?

I started with POS: (a+b+c)(a+b'+c)(a'+b+c)(a'+b+c') and after a long while, I got: ab+ac'+a'b'+a'c+b'c'+bc and then I'm not sure how to simplify this. I thought maybe I can cancel the ab with a'b', ...
2
votes
1answer
91 views

Propositional logic — syntactical completeness

Lets consider propositional logic. We say a proof system for propositional logic is syntactically (negation) complete if for every $\alpha$, either $\alpha$ or $\neg \alpha$ are provable within the ...
4
votes
2answers
77 views

What is the definition of a $\Pi_1$-sentence?

What is meant when somebody says that a problem can be expressed as a $\Pi_1$-sentence? I know that for the arithmetical hierarchy, a $\Pi^0_1$-sentence is a sentence of the form $\forall n_1\forall ...
0
votes
1answer
33 views

Descriptive complexity: 3-colorability example

So in Neil Immerman's book http://books.google.co.kr/books?id=kWSZ0OWnupkC&pg=PA113&lpg=PA113#v=onepage&q&f=false, 3-colorability problem in descriptive complexity fashion is expressed ...
0
votes
2answers
42 views

Recursive equations vs. inference rules

It seems to me that recursive equations can always be presented as inference rules. For the forward direction, an example is addition over Peono numerals (built from $O$ and $S(\_)$) $$ ...
0
votes
3answers
39 views

A graph in descriptive complexity - is $x$ already a vertex?

So suppose that there is an undirected graph with edge connections known. Now in first-order logic there is quantifier $\forall x$. Then does this automatically refer to vertexes, or can we use ...
1
vote
1answer
45 views

How to prove that a predicate is prefix closed

Suppose we have the predicate $\qquad A.p.q ≡ (∀i \mid p≤i≤j<q : X.i≤X.j)$ which says that $X[p..q)$ is ascending. Apparently, the predicate holds for empty segments, is prefix closed and is ...
3
votes
3answers
423 views

Does a logical system have semantics?

From Wikipedia: A logical system or, for short, logic, is a formal system together with a form of semantics, usually in the form of model-theoretic interpretation, which assigns truth values to ...
2
votes
1answer
44 views

Does Herbrand's theorem mean any first-order logic formula can be expressed in CNF?

Herbrand's theorem shows that any formula of first-order logic can be expressed as a disjunction of quantifier-free formulas of first-order logic. Is this equivalent to saying that Herbrand's theorem ...
4
votes
1answer
36 views

First Order interpretation of arbitrary structures as a graph

I am currently trying to get some intuition on the concept of First Order reductions, and have come across this exercise question by Immerman, dubbed "Everything is a Graph". Given some arbitrary ...
-2
votes
2answers
90 views

Example for an unsatisfiable formula that can be made satisfiable by reordering quantifiers [closed]

Please give me an example of an unsatisfiable quantified 2 CNF formula. I need it in my proof and I am unable to think of one. I am looking for such an unsatisfiable quantified 2 CNF formula which ...
3
votes
1answer
61 views

Can quantified renamable Horn formulas be identified using the same procedure as unquantified formulas?

Definition: A renamable Horn formula is a Boolean formula that can be transformed into a Horn formula by flipping the polarity of every instance of one of more of its variables. Example: $\qquad ...
0
votes
0answers
41 views

How to ascertain that the result of 1's complement arithmetic is invalid/valid

Trying to do (5)$_{10}$-(-5)$_{10}$ in 4 bit 1's complement system: 0101-1010 = 1011 with borrow 1 Subtracting back borrow 1011 - 1 = 1010 So sign bit is 1 in final answer, thus in 1's ...
-3
votes
1answer
41 views

Why is Mixed Quantified Horn SAT in PSPACE?

I want to prove that Mixed Quantified Horn SAT is a PSPACE-complete problem. I have proved that it is PSPACE-hard. How can I prove that it is in PSPACE? My study: To prove QSAT to be in PSPACE: ...
0
votes
1answer
110 views

Concept used in the proof [closed]

In the paper "Resolution for Quantified Boolean Formulas", I am unable to understand the proof of theorem 3.4. Please help me with the basic concept used on page 4: The concept that I am referring ...
3
votes
2answers
84 views

Composition of combinators with arities greater than one

In combinatory logic, the axiom of composibility asserts that for any two combinators, $A$ and $B$, there exists a combinator $C$ that composes $A$ and $B$. That is, for all $A,B,x$ there exists a ...
0
votes
1answer
42 views

How to design xml schema for digital circuits? [closed]

how can i design XML Schema for logical and digital circuits? i cant find any help or manual for this work for example i have a digital circuits with AND OR NOR ,... gates now i want design xml ...
1
vote
0answers
46 views

Translation of natural language to logic [closed]

Given a statement in natural language, what can be said about how many possible translations there are in first-order-logic? What happen if we take a more complex logic like second-order logic and ...
2
votes
1answer
80 views

Solving SAT using tableau calculus

I've learned about tableau calculus which is a decision procedure solving the problem of satisfiability of a first order logic formula. Now I'm wondering why this technique can't be used to solve the ...
-2
votes
1answer
80 views

Quantifier String Placement [closed]

This is the edited question: Suppose I have $(x_1 \vee y_1 \vee y_2)$. x is existential and y is universal. Then it should be like this in the quantifier string: $\forall y_1 \forall y_2 \exists x_1$ ...
4
votes
3answers
175 views

What is wrong with this seeming contradiction with a paper about AND-compression of SAT?

EDIT 3: Might be wrong, but I am still confused by the answer's claim "It does not have to output an instance that preserves all satisfying assignments for all the input instances". This appears to ...
7
votes
3answers
934 views

Gödels (first) incompleteness Theorem and the Halting Problem - How limiting is it?

When I first heard of these things I was very fascinated as I thought it sets really a limit to mathematics and science in general. But how practically relevant are these things? For the Halting ...
1
vote
5answers
189 views

Real life description for (~A->A)->A

It can be shown that the logical preposition [ :- (~A->A)->A ] is a theorem (always true). I want to know if anybody knows a real life description for the preposition above? I mean an expression in ...
4
votes
1answer
64 views

Showing that a Particular Word Problem is Decidable

I need to give an algorithm to show that the word problem in the group $\langle x,y \mid \mid x^{1984} = y^{2014} = 1 \rangle$ is decidable. How do I show this? I'm not too sure where to start.
8
votes
1answer
83 views

Hilbert's 10th Problem and Chaitin's Diophantine Equation “Computer”?

In Chaitin's Meta Math! The Quest For Omega, he briefly talks about Hilbert's 10th Problem. He then says that any Diophantine Equation $p=0$ can be changed into two equal polynomials with positive ...
2
votes
0answers
44 views

Introductory book on Logic and Computation

Can you give me some suggestions about a good introductory (but comprehensive) bookabout Logic and Computation? Some fuzzy topics that I have in mind are: Presburger artihm., PA, ZF, ZFC, HOL Set ...
2
votes
1answer
342 views

Consistency and completeness imply soundness?

I understand that soundness implies consistency. Also, I understand that consistency alone does not imply soundness. But shouldn't consistency + completeness imply soundness? Scott Aaronson in his ...
1
vote
1answer
61 views

Logic applications and security protocols references request

I'm a student of logic and I'm interested in looking at logic applications, of which I am told there are many, in computer science and allied areas. I've seen some applications. More specifically, I ...
1
vote
0answers
17 views

Extending the type scheme for Burks/Warren/Wright machine to handle operators on functions?

Some background: Burks, Warren and Wright published a description of simple interpreter for a Logic Machine for unparenthesized Lukasiewicz notation (paper, SO question, c implementation, postscript ...
4
votes
1answer
35 views

Should we not reuse constants in tableaux proofs?

I am trying to understand the proof of the following using tableaux: $$ \exists x\forall y.r(x,y) \to \forall x \exists y . r(x,y) $$ This is how it works out: $$ (1) \space \exists x \forall y ...
1
vote
1answer
37 views

Satisfiabilty 2-sat

Im trying to work out whether the following clause is satisfiable: {x, y},{x,¬y},{¬x, y},{¬x,¬y},{x, z},{x,¬z},{y, z},{y,¬z} My basic understanding is to work ...
2
votes
1answer
131 views

Create a shallow logic circuit that increments a binary number

This circuit should be reasonably efficient in size and depth, but with priority on depth. If depth was not a concern, then I guess I could make a specialized adder for the least significant bit and ...
1
vote
0answers
54 views

Propositional logic of arguments and undercuts [closed]

The setting An argument from a set of formulas $\Delta$ is a pair $\langle \Phi, \alpha \rangle$ such that $\Phi \subseteq \Delta$ $\Phi \nvdash \bot$ $\Phi \vdash \alpha$ (this is what I am ...
5
votes
1answer
78 views

Finding a graph-theoretic representation of expressions in Boole's algebra

I just read "Boole's Algebra Isn't Boolean Algebra" by Theodore Halperin (behind a paywall here). I don't have a strong background in abstract algebra, so, frankly, the paper is a bit over my head but ...
0
votes
1answer
32 views

Finding a finite model

Hello I am having difficulty with this question, I am not even sure what strategy one would go about proving something like this: Suppose $L$ is a language which includes an infinite list ...
3
votes
1answer
31 views

LK-$\phi$ proof of $\exists y Pby$

I am having difficulty with the concept of $LK-\Phi$ proofs, here is a question I have been working on: Let $\Phi = \{Pafa\}$, where $P$ is a binary predicate symbol and $f$ is a unary function ...
0
votes
1answer
65 views

Odd Parity Function [closed]

I am trying to define a Odd Parity Function that takes three 1 bit inputs and will output a 1 if the 3 bits are odd as a Boolean function. ...
2
votes
1answer
55 views

FOL substitution - is it possible to substitute two variables with each other? e.g. $\theta=\{x/y,y/x\}$?

Let $C = m(P,X,Y) \leftarrow m(Q,X,Z), m(R,Z,Y)$. Is it possible to do the following substitution? $D = C\theta$ where $\theta = \{Q/R,R/Q\}$ s.t. $D = m(P,X,Y) \leftarrow m(R,X,Z),m(Q,Z,Y)$
2
votes
1answer
57 views

3-coloring a graph with propositional formulas

I am trying to tackle a specific problem so any help would be greatly appreciated: Let $G = (V,E)$ be an undirected graph with vertex set $V$ and edge set $E$. A 3-coloring of $G$ is a map ...
1
vote
1answer
64 views

Application of Combinatorics, Logic and computability theory in physical science: Tiling of Wang Tile with proportionality [closed]

The original problem of Domino Tiling and Wang Tile has great theoretical interest on computability theory... However, the great emerging problem on application of Wang Tile in material science and ...
1
vote
2answers
61 views

Can we move quantifiers to the left in predicate logic?

Say I have part of a query in the form: ∃xa(...)∧∃xb(...)∧∃xc(...), where a, b, and c are attributes and the ellipses can be anything (I'm looking for a general rule). Is this equivalent to saying ...
0
votes
0answers
28 views

Are these CNF clauses for at most one and the same correct?

Given Boolean variable Xij that represents whether dog i is kept in kennel j. Encode in CNF clauses: Dogs that cannot be kept together must be kept in separate kennels Here is what I ...
3
votes
2answers
63 views

Constructively deciding whether a decidable predicate holds universally

I am trying to obtain the proof of the proposition: $(\forall x \in \mathbb{N}, P(x)) \vee (\neg \forall x, P(x))$ given that the property $P$ is decidable for every $x \in \mathbb{N}$, i.e. ...
3
votes
1answer
42 views

grammatical complexity of propositional and monadic predicate validities? (and grammars for recursive but not context-sensitive languages?)

Consider two sets: the set of validities of propositional logic and the set of validities of monadic predicate logic. Call the first set $VP$ and the second set $VQM$. Both of these sets are ...