Stack Exchange Network

Stack Exchange network consists of 174 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

3
votes
1answer
69 views

Why use logic gates in this situation? (XOR gates)

I came across this circuit that swaps logical signals: However I don't understand why would you need to use logic gates. Would it be possible to just connect the A on the left to the B on the right ...
0
votes
2answers
54 views

What are constraints on some new logic programming language and system?

As I understand, everyone can create logic programming language and system by declaring that the valid program of some logic programming language is the set of statements in the form: ...
3
votes
2answers
78 views

Predicate Logic - Natural Deduction; Assumptions about exists-elimination

I am stuck on how to progress with this proof; i cannot see my next move. The task is to show $S \to \exists x Q(x) \vdash \exists x (S \to Q(x))$ using natural deduction for predicate logic. My ...
0
votes
1answer
28 views

How to solve for the precondition give a postcondtion that must satisfy two conditions

I tried solving past exam question but there is this one that I haven't been able to solve. The question states that a suitable precondition should be found for the statement. $$ a= i +2; i++\{(a = ...
0
votes
0answers
32 views

Writing LTL formula for sequencing with coordination

Suppose there are 2 workers w1 and w2 who can cool a hot iron. So if iron is hot (denoted by atomic proposition ...
3
votes
3answers
84 views

Represent there are infinitely many in FOL

How to represent in first order logic the expression: "there are infinitely many" To be honest I'm confused and not even sure whether you can represent them in first order logic.
-1
votes
1answer
34 views

Optimization problems and quantifiers

A simple optimization problem is of form $\max_{x\in\mathcal R}f(x)$. We can quantify as $\exists x\in\mathcal R\forall y\in\mathcal R f(y)\leq f(x)$. The quantification here is $\exists\forall$. ...
0
votes
2answers
49 views

Easiest way to find y in $x \text{ xor } y = z$ with given $x \text{ and } z$

Let's say we have given two numbers $x, z$, and we need to find another number $y$ such that $x \text{ xor } y = z$. The xor ( exclusive or ) is bitwise operation: xor table . I know that this can be ...
0
votes
1answer
70 views

Are there any implementations of computability logic?

I'm currently looking into Japridze's computability logic. It looks great, but I was wondering whether any programming languages or systems implement it. Does anyone know of any implementation? ...
6
votes
2answers
1k views

Why does the copycat strategy work for two parallel chess games?

I'm currently looking into computability logic. Japaridze explain that a game !P v P like !Chess v Chess is always winnable thanks to the copycat strategy (http://www.csc.villanova.edu/~japaridz/CL/3....
0
votes
1answer
41 views

Boolean expression to a truth table

How do I fill a truth table from the following expression? I can't decide whether it is SOP or POS. Y=(A+B)C+AB`+(A+C)C`+(`AB)
6
votes
2answers
171 views

Does Provable P equal Provable NP?

My question is a very basic one. It seems feasible to believe that $\mathsf{P = NP}$, because there is some "pathological" good algorithm for SAT, yet it is impossible to prove that the algorithm is ...
0
votes
1answer
28 views

binary max and binary min [closed]

I'm reading a paper about constraint satisfaction problem and found a term "binary Max and binary Min" operations but I dont know the meaning. If someone know could you please explain for me? I ...
4
votes
1answer
123 views

Logical characterization of P versus NP problem (and references for least fixed point logic)

Wikipedia says the following (and more) about the logical characterization of the P versus NP problem here: Thus, the question "is P a proper subset of NP" can be reformulated as "is existential ...
2
votes
0answers
48 views

Why, intuitively, is Lob's theorem true? [closed]

Lob's theorem states that: Let $\textbf{Prov}(n^A)$ be the arithmetic statement such that $PA\vdash$ $A$ iff $\textbf{Prov}(n^A)$, where $PA$ is peano arithmetic, and $n^A$ is the godel number of $A$....
0
votes
0answers
15 views

Converting CNF boolean expression into DNF and vice versa [duplicate]

Is there any algorithm for converting a DNF boolean expression to CNF and vice versa if it's exists what is time complexity and complexity class for solving this problem?
-2
votes
2answers
36 views

How to specify a robot go always right relative to itself from absolute perspective (north west east south)

I have a robot that has a start and goal position within a maze. Each point in the maze-grid is simply a Position object containing x and y. I need an algorithm that specifies the robot only moving to ...
0
votes
0answers
10 views

Techniques used in customizing Task Scheduling

I am just learning about Scheduling, in particular the Completely Fair Scheduler. In thinking of specific cases of the types of things that would need to be "prioritized" against each other, there ...
1
vote
0answers
21 views

Is it possible to define logic programming for every logic that has implication and conjunction connectives?

Is it possible to define logic programming for every logic that has implication and conjunction connectives? Does logic programming adds something new to the usual inference process. By usual ...
8
votes
2answers
697 views

Why doesn't Godel's Second Incompleteness Theorem rule out a formalizable proof of P!=NP?

I'm sure there must be something wrong with the following reasoning because otherwise a lot of P vs. NP research would be curtailed but I cannot determine my error: For any fixed integer $k>0$ ...
2
votes
1answer
97 views

Least fix point of CTL formula

In the book Logic in Computer Science on page 244, there is a proof that $[[E(\phi U\psi)]]$ is the least fixed point of $G(X)=[[\psi]] \cup ([[\phi]]\cap\mathop{\textrm{pre}}_\exists(X))$. I don't ...
0
votes
1answer
47 views

Maximum number of distinct values for bitwise OR

You are given an array with $N$ elements. The values of the elements may be any number in the interval $[0,10^9]$. Define $f(a,b)$ as the bitwise or of all the values in the subarray $[a,b]$. Find a ...
1
vote
2answers
50 views

Can an FO formula with infinite length be expressed with an infinite set of finite formulas?

I'm confused as to why we can't write formulas of infinite length in FO. For example, to express reachability, I understand the proof that there cannot be a single formula for it, but it is ...
1
vote
2answers
130 views

Is the halting problem theorem really proven

Here is a popular proof of the halting problem theorem: Suppose there exist a procedure h(x, y) so that for any procedure p(x) and any data d, the execution of h(p, d) will halt, where halt means ...
1
vote
0answers
39 views

Understanding a Single Step in the Model Checking Algorithm

This answer explains roughly how to convert a nested boolean function into a Binary Decision Diagram (BDD). This question is about how to structure the states for the BDD. Now in this question I am ...
2
votes
0answers
112 views

Equivalence preserving operator from CTL* to LTL

The question is about an operator that transforms any CTL* formula ${\psi}$ into a (not necessarily equivalent) LTL formula ${A\psi^d}$, where $d$ means syntactically removing all $A,E$ quantifiers ...
2
votes
1answer
19 views

Unclear logic notation for PFX program rules

I'm very new to this so please bear with me. I found this document describing the PFX language, a stack-oriented language where the instructions act on a stack and replace the arguments with the ...
1
vote
1answer
33 views

Operation with second-order logic formulas

I have one or more second-order logic formulas that correct for some finity model. What operation can I perform on them, so that resault is also correct for some finity model? Just conjunction is ...
1
vote
1answer
39 views

Can agent be autonomous without having consciousness?

My intuition is that 1) self-awareness (modeled through epistemic modal logics); 2) goal reasoning (e.g. https://www.aaai.org/ocs/index.php/AAAI/AAAI16/paper/view/12292) and 3) consciousness (e.g. ...
1
vote
0answers
30 views

How to apply Hoare Logic to this function

I would like to apply Hoare Logic to realistic, complex imperative programs that use while loops, if statements, functions, modules, etc. and have side effects (e.g. access the network). In order to ...
0
votes
1answer
51 views
2
votes
2answers
57 views

Subtlety of a bar in introduction rule

I am going through the following lecture notes by Frank Pfenning : http://www.cs.cmu.edu/~fp/courses/15317-f17/lectures/02-natded.pdf In page no 5 I cam across the introduction rule . The rule ...
0
votes
1answer
33 views

Provide a derivation from backwards on?

Suppose you have to provide a derivation by natural deduction, e.g. $((A \rightarrow B) \rightarrow A) \rightarrow A$ Is it a good advice to start from backwards on in general? I mean doing the ...
1
vote
1answer
33 views

How to express a structure of a 5-colorable graph in logic

A graph can be expressed as an structure $G = <A,R>$ satisfying the axioms $ \forall xy R(x,y) \rightarrow R(y,x)$ and $ \forall x \lnot R(x,x)$. How to extend the structure and/or axioms to ...
0
votes
0answers
20 views

Why are there so many different computer programming languages? [duplicate]

This is for a school project, please help. I have looked this up, but haven't gotten a good answer.
-2
votes
1answer
41 views

What is Control ROM and Decision ROM?

I have done some research but I cannot answer this question. Please Help.
1
vote
1answer
31 views

Resolution Algorithm - No new clauses

The standard resolution algorithm returns false if no new clauses are added. I know that if $KB \land \neg a \implies []$, it returns true by proof by contradiction, but how can I understand the ...
3
votes
0answers
38 views

Expressing definite clauses (Horn rules, logic programming) in lambda terms?

There is paper which expresses lambda terms in the terms of logic programming http://www.cse.unt.edu/~tarau/teaching/PL/docs/dbx.pdf Is there conversion in the other direction - expressing definite ...
1
vote
1answer
57 views

Optimal 4-input sorting network

In his paper The Bose-Nelson Sorting Problem (1973, Chapter 15 of A Survey of Combinatorial theory on page 163 available on Google books), Knuth says that the optimal bound of 5 comparators for a 4-...
4
votes
1answer
675 views

Why is this expression (A and ¬A |= C) entailed?

Hopefully I am posting this in the right place, I am currently in a course of knowledge representation, and I came across an exercise about entailment: $$A\land\neg A\vDash C\,.$$ I would argue that ...
1
vote
1answer
63 views

Can the higher-order oracle Turing machines simulate the lower-order machines so that the current oracle does not contradict the simulated oracle?

Here is a quote from the Source 1: For example, if $M$ is a machine with an oracle for the halting problem, then obviously there isn't in general an equivalent machine that can simulate the ...
2
votes
1answer
110 views

Trying to understand interpretation and denotation in FOL

I am going through the book "Knowledge Representation and Reasoning" by Brachman and Levesque. So an interpretation $ F $ is defined as a pair $ \langle D,I \rangle $ mapping from a set of objects $ ...
1
vote
2answers
59 views

The set of valid sentences in FO is not decidable as a consequence of rec. inseparability

Two given languages $L_1$ and $L_2$ are called recursively separable iff there exists a recursive languge $R$ such that $L_1 \subseteq R$ and $L_2 \cap R = \emptyset$. Now consider first order logic, ...
2
votes
0answers
95 views

Is there an analysis of the creation of axioms for a mathematical structure as a computational problem?

Historically, what has happened is the following: There is a "mechanical" structure, most importantly, arithmetic, which operates according to a set of well-defined rules that a stupid computer can ...
0
votes
1answer
62 views

LTL to automaton translation that can only read disjunctions of labels per transition

Is there any automaton (or automaton translation) as expressive as LTL that can only read disjunctions of atomic propositions per each transition? Standard LTL-to-automaton algorithms allow the ...
0
votes
0answers
48 views

What are transitive roles in description logic?

I've begun to study Description Logic recently and there are a huge number of new terms to me. One of these terms is transitive role. I found this term in slide 7 and my question is: what is ...
0
votes
1answer
53 views

box bottom is valid

This question was posted to me: What property of our relation $R$ between worlds must be true if we know that the following formula is valid? $\square \bot$ I am completely stumped and have no idea ...
2
votes
1answer
58 views

Complexity of Solving a System of Polynomial Equations

It can be easily seen that solving systems of polynomial (i.e. not necessarily linear) equations is NP-Hard via reduction from SAT. Furthermore, because the existential theory of the reals is ...
34
votes
3answers
5k views

What exactly is a logic?

An apology might be in due for asking another question about prerequisites, but I was confused about the starting points. I have come across various terms such as "Modal Logic", "Temporal logic", "...
10
votes
0answers
243 views

Is Agda sound as a proof system?

I was browsing Agda's stdlib source code, since I was trying to get into it seriously and therefore wanted to know more. I was amazed at that Agda is way more developed than I thought and it's ...