Questions related to logic and its use in computer science

learn more… | top users | synonyms (1)

1
vote
1answer
50 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
44 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
19 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
46 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
32 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 ...
1
vote
4answers
79 views

How can I prove $P \rightarrow (Q \rightarrow R)$ is equivalent to $(P \wedge Q) \rightarrow R$

I'm a freshman CS student at my university and i'm struggling with understanding my professor through his thick accent. I've asked him to explain the proof for this multiple times and still have ...
3
votes
2answers
54 views

Unification — most specific unifier

In unification, given a set of equations, a standard problem is to compute a most general unifier (mgu). I am interested in a somewhat reversed problem. Imagine having a set of equations that do not ...
4
votes
2answers
188 views

P, Q, ((P→Q)→R) ⊢ R using only modus ponens

Can $R$ be inferred from $P$, $Q$, and $(P \to Q) \to R$ using only modus ponens? My understanding is that it can, as shown below, but I was told this was incorrect. Proof of ${P, Q, (P \to Q) \to R} ...
5
votes
1answer
250 views

How does binary addition work?

I find binary confusing. I have watched minecraft redstone videos on binary adders, real binary adders, diagrams, etc and yet I have not learned much at all. How does electrons flowing through wires ...
0
votes
1answer
11 views

Modelling 2 object situation with Propositional Logic

I'm reading up on propositional logic, and I'm completely stuck on this example - spent the past few hours trying to figure it out! Any pointers would be appreciated. There's 2 trees, each with signs ...
4
votes
2answers
38 views

Mapping intuitionistic logic to the modal logic S4

In his famous Semantical Analysis of Intuitionistic Logic, S. Kripke speaks of the "well-known mappings of intuitionistic logic into the modal system S4". I'm not sure which mappings Kripke means. One ...
11
votes
4answers
187 views

Has Anyone Actually Created a System that Writes Computer Programs from specification?

Has anyone ever actually written a system (software or detailed explanation on paper with simple examples) that generates computer programs? I input $Prime(x) \wedge x<10$ and it creates a program ...
6
votes
0answers
29 views

Boolean formula that agrees with most truth assignments

Let $X_1,\dots,X_n$ be $n$ boolean variables. I have an unknown predicate $P(X_1,\dots,X_n)$ on these boolean variables. Of course, I can view the predicate as a function $f_P : \{0,1\}^n \to ...
-2
votes
1answer
73 views

Karnaugh map - assign variables to the inputs?

I drew the map on the right, but what I drew doesn't work for what the question is asking me. I think I did something very wrong, and I don't really understand what this question is asking me. Am i ...
1
vote
1answer
36 views

assertion in first order logic

Can anybody give me an idea how to write this assertion in in first order logic? X has not passed one or more of the prerequisites for A. Here, X is the name of a person and A is a constant ...
5
votes
2answers
72 views

Number of instances of SAT (boolean satisfiability) problems of size N?

I assume the size of an instance of the SAT problem is measured by its number of (Boolean) variables. What is total number of instances of SAT problems of size N? I guess that amounts to counting ...
1
vote
1answer
29 views

Recognizing Horn clauses

I am currently studying model theory and I am trying to decide if a clause is a Horn Clause. I know that a Horn Clause is a clause with at most one positive literal, but there are some clauses that it ...
2
votes
1answer
29 views

Finding the minterm expression of F + G [closed]

I have a question that asks me to find the minterm expression of two functions added together. The two functions in this case are F = m(0,4,5,6) G = ...
3
votes
1answer
170 views

Why ⊢ for affirmative predicates and ⊨ for ¬negations?

I read a book which says that in Predicate Calculus, syntactic theorem proving is identical (complete and sound) with semantic entailment and this is very useful because it is easier to prove positive ...
1
vote
1answer
33 views

Logic Question - Why is This an Implication?

I have a question about predicate logic. Suppose we have the following predicates: $\text{Study}(x,y)$: x studies y $\text{Comp}(x)$: x is a computing student I want to encode the following ...
1
vote
2answers
66 views

Applications for boolean logic operations in zero-one integer linear programming (ILP) [closed]

It is nice to know that every boolean formula can be expressed by zero-one integer programming by this answered question. But are there any applications? To be more precise: Are there papers which ...
1
vote
1answer
35 views

Until quantifier of Computation Tree Logic

It's quite a short question: Refering to this Wikipedia article p U q means, that p has to hold at least until at some point ...
1
vote
1answer
48 views

Computation tree logic and Kripke structures

Specifications in Kripke structures are verified by Computation tree logic (CTL). However, refering to this Wikipedia article the CTL-operators are relative to a current state. So, when we want to ...
1
vote
2answers
68 views

What's an example of an unsatisfiable 3-CNF formula?

I'm trying to wrap my head around an NP-completeness proof which seem to revolve around SAT/3CNF-SAT. Maybe it's the late hour but I'm afraid I can't think of a 3CNF formula that cannot be satisfied ...
4
votes
2answers
56 views

Positive term for “unnegated”?

I read a paper which talks about "a logic formula in which each variable appears at most twice unnegated and once negated". The term "unnegated" is double-negative, which makes it slightly unclear. Is ...
6
votes
2answers
77 views

How strong is equivalence of lambda expressions?

Consider two lambda expressions $\mu$, $\nu$ representing computable functions $f_{\mu,\nu}:\mathbb{N} \rightarrow \mathbb{N}$. If $\mu$ and $\nu$ are equivalent under the combination of ...
1
vote
1answer
48 views

Transition systems that satisfy LTL but not CTL, and vice versa

I am learning about temporal logic and model checking systems. One conceptual exercise that I am struggling with is how to create a transition system which satisfies only one of two given properties, ...
1
vote
1answer
37 views

Normal order sequencing vs applicative order sequencing

I'm trying to understand this lecture, section 2.7. Why would the normal order sequencing print out "hello" "world" and not ...
1
vote
2answers
65 views

Computation Tree Logic and its Temporal Opeators

I've got some questions about the temporal operators in computation tree logic: Does the Finally path-specific quantifier Fq ...
5
votes
1answer
29 views

Simply Typed Combinatory Logic?

As there is an untyped lambda calculus, and a simply-typed lambda calculus (as described, for example, in Benjamin Pierce's book Types and Programming Languages), is there a simply-typed combinatory ...
2
votes
1answer
69 views

Why do they say `A, B, C, … implies M` instead of `A∧B∧ C∧ … implies M`?

The conclusion follows from all the premises. It seems to me that this means that conclusion from the conjuntion of the premises. Right? Why does logic uses comma instead?
2
votes
4answers
152 views

No number is equal to Zero, is this statement true or false?

While reading an article on logic, there is a sentence "No number is equal to zero" and we have to assign truth values to this sentence. I hope this is true and the article says it as false. Can ...
-1
votes
0answers
21 views

Kripke Structure and Temporal [closed]

Here is a Kripke structure M over AP = {a,b,c} ...
0
votes
1answer
60 views

Converting English into Logic

I'm learning about Logic; I've devised a few sentences to convert into logic to test myself and see if i've grasped the topic. It would be of great help if you could tell me if i'm doing it right! ...
-2
votes
1answer
62 views

Alternative representations for the zebra puzzle?

All of the solutions for the zebra puzzle have a variable for each of the properties and a domain with the possible values. For instance A for Nationalities, B for pets, ... Ai with i = 1..5 and the ...
0
votes
0answers
424 views

Simplifying a boolean function with don't care using K-map in SOP and POS form

Simplify the boolean function using the K-map of $F$ together with the don't care condition $d$: $F(A,B,C,D)=\Sigma(1,2,3,4,19,11,12,13)$ $d(A,B,C,D)=\Sigma(0,6,7,8,9)$ a) In sum of ...
5
votes
0answers
61 views

On the Turing Completeness of First Order Logic

It is well known that in Descriptive Complexity Theory FO is equivalent to AC0. However, this accepts a couple of a theory and a string <T,s> iff the ...
0
votes
0answers
61 views

Introductory book to fuzzy logic for Artificial Intelligence

I need to study fuzzy logic and its application in the field of A.I. I'm reading "First Course On Fuzzy Theory and Application" (pdf) (WorldCat), but not much of examples there and I couldn't find a ...
0
votes
3answers
86 views

Resolution and what it means to derive the empty set

When using resolution, if the empty set {Ø} is derived from a formula like {¬x,¬y} {x,y}, does that mean the formula is unsatisfiable? If this is the case, why is ...
1
vote
1answer
95 views

Shouldn't the “even parity” function map 1101 to 0?

From the book Computer organization and design by Patterson&Hennessy: Parity is a function in which the output depends on the number of 1s in in the input. For an even parity function, the ...
0
votes
1answer
170 views

Drawing an implication graph for 2-SAT clauses

I am trying to convert the following 2-sat clauses to implications and then draw the implication graph. The clauses are: ...
1
vote
1answer
64 views

Multivalued, partial evaluation

Everybody says that Valuation is a truth value assignment to all variables in the formula. How do you call the valuation when some (neither single yet nor all) variables are assigned a value? ...
9
votes
1answer
108 views

Verify correctness of quantifier elimination, using SAT

Let $x=(x_1,\dots,x_n)$ and $y=(y_1,\dots,y_n)$ be $n$-vectors of boolean variables. I have a boolean predicate $Q(x,y)$ on $x,y$. I give my friend Priscilla $Q(x,y)$. In response, she gives me ...
2
votes
1answer
38 views

Counting involving equivalence classes and languages

Let $\Sigma$ be the alphabet $\{a, b, c, d\}$ and let $R$ be the following relation on $\Sigma^*$: $R(x, y)$ is true if every letter in string $x$ also occurs in $y$, and every letter in string $y$ ...
8
votes
3answers
298 views

Intro to Martin-Löf type theory

What would be the best introduction to Per Martin-Löfs ideas about type theory? I've looked at some lectures from the Oregon PL summer school, but I'm still sort of puzzled by the following question: ...
4
votes
1answer
47 views

Abduction in ASP

Well, forgive my ignorance about the matter as I have been playing with ASP for the last couple of days. Consider this simple example p. s :- p. And the ...
4
votes
1answer
114 views

Characterising $(aa)^*$ in first order logic

In my descriptive complexity class, we've been asked to find a formula that characterises the language $(aa)^*$ (over the alphabet $\{a\}$) with a first order formula over the language $\{<, ...
1
vote
1answer
142 views

Fundamental Boolean Functions

I can define any boolean function (I think) using and and not, or using or and not (plus a constant 0 or 1). And I can define or in terms of xor. And then there are nor and nand. So I am wondering: ...
2
votes
1answer
114 views

What is the name of this combinator?

I've recently started casually reading into combinatorial logic, and I noticed that a higher-order function that I regularly use is a combinator. This combinator is actually pretty useful (you can use ...
1
vote
0answers
38 views

Inversion of BDD

How can I write an algorithm which inverts a 2-level BDD? It should take as input a 2L-level quasi-reduced BDD rooted at $r$ encoding a relation $R : B^L → 2^{B^L}$ and returns the 2L-level ...