Questions related to mathematical logic and its use in computer science
0
votes
0answers
8 views
How express this short sentence in CTL?
It's possible that in some following state you have that $x,y$ are
both true simultaneously.
I have taken a look on Wikipedia: https://en.wikipedia.org/wiki/Computation_tree_logic
and if I ...
0
votes
0answers
12 views
Propositional extentionality in the lean theorem prover?
Propositional extentionality in the lean theorem prover is stated as the following axiom:
axiom proptext {a b : Prop} : (a $\iff$ b) \to a = b
My confusion about this is as follows: Previously I’...
2
votes
1answer
24 views
How do you correctly write this sentence as a CTL formula?
Sentence: From every reachable state it is possible to reach a state where $p$ is true.
How do you write this sentence as a CTL formula? So far I only dealt with CTL syntax and trees but maybe it ...
0
votes
0answers
18 views
Type theory based automated theorem prover?
I know that there exist type theory based proof-checker, and I know that there are logic/sequent-calculus based automated theorem provers.
But I haven’t heard of a type-theory based automated theorem ...
4
votes
1answer
40 views
A universal operator necessarily generates $\neg x$ for input $x,…,x$
I originally posted this on math.stackexchange, but then deleted it and moved it here since I think it would fit this site more.
I saw a claim in a slideshow from a basic computer architecture course ...
4
votes
1answer
84 views
Is there a way to convert a program into a Boolean formula?
Let's say I have a program P, in form of a binary code for x86 architecture.
I want to find a Boolean formula F (in form of CNF, or something like that), such ...
1
vote
1answer
89 views
Given a rng that outputs 0 or 1 with an equal probability, make a rng that generates 1 with a probability p
So this was an interview question I had a few weeks back that I just haven't been able to think of how to solve...
Given a random number generator that returns 0 or 1 with a 50% chance of either, ...
1
vote
0answers
24 views
How to minimize large DNF formula into deeper but smaller formula?
I want to minimize DNF formula which has ~200k products combined into a sum.
The depth of that formula is 2 - first level is the OR, and second level is AND for all conjunctions.
I have tried using ...
0
votes
1answer
27 views
Logic gate which checks if the input is a negative number and changes its output based on that
I need to create a HDL which will use logic gates to demonstrate if something is a negative number in two's complement. The input is 8 bits, while the output is 1 bit, and if the input is a negative ...
0
votes
1answer
14 views
What if an $L$-complete problem has $NC^1$ circuits? More generally, what evidence is there against $NC^1=L$?
What if an $L$-complete problem has $NC^1$ circuits? More generally, what evidence is there against $NC^1=L$?
3
votes
0answers
32 views
An instance when you can eliminate propositional double negation in coq
Suppose st: string -> nat and X stands for the string 'X'.
Given the hypothesis ...
0
votes
0answers
28 views
Logic unification with list
So I am studying for an exam which includes unification. I am fairly confident in unifying and calculating the mgu. But I am having trouble understanding how to prove if the following is unifiable or ...
0
votes
1answer
24 views
Boolean Algebra Simplifying complex equation
I am trying to simplify the following equation and I am getting stuck on a line and I can't cut it down any further. I'm not sure if certain 'moves' are legal or not.
F(A,B,C,D) = A'B'C' +ACD + A’BCD ...
2
votes
1answer
83 views
How to represent symbolic knowledge using real numbers - theory about neural networks and natural/analog computing?
One can define the semantics of one definite word using the references to real world entities, relationships with the other words and other concepts and represent all this knowledge about this one ...
1
vote
2answers
52 views
How to define (logically) the complement language?
I found it a little bit difficult and confusing to define the complement language in specific cases. For example, take the next language:
$$L = \left\{\langle M, w\rangle \;\middle|\; \begin{array}{...
1
vote
1answer
45 views
Relational calculus to SQL
I am somewhat aware of the correspondence between (tuple and domain) relational calculus, relational algebra, and SQL. To the best of my understanding, one should be able to automatically convert a ...
-3
votes
1answer
62 views
Is it there any computer/cellular automaton/brain to compute logically impossible and incomputable things? [closed]
Is it there any computer or cellular automaton or model of the brain where they could compute logically impossible things and incomputable things?
For example, if we wanted to compute/simulate/think ...
1
vote
1answer
34 views
What's the output of this algorithm?
Given the question below:
Consider that, on the procedure below, the variable X is defined globally and the parameters of the vr function are passed by value
...
0
votes
1answer
66 views
Understanding SLDNF-forest
I am trying to understand this program and the respective forest. This is from the book Logic,Programming and Prolog by Ulf Nilsson.
Question:
In the main tree, why from ←off_gound(a) can you ...
11
votes
1answer
248 views
“Famous logicians have made embarrassing errors here,” a line from SICP. What is this referring to?
Here is the context (Structure and Interpretation of Computer Programs, section 1.1.8, under heading "Local names"):
A formal parameter of a procedure has a very special role in the procedure ...
3
votes
0answers
39 views
A book introducing proof theory needed (many-sorted FOL, classical non-Gentzen calculus, satisfiability in partial algebras, induction)
We define a signature as a triple $$\Sigma\ =\ (S,F,\mathrm{type})$$ where $S$ is a set of sorts, $F$ a set of $n$-ary function symbols $f$ of the type $\mathrm{type}(f)$ $=$ $(M_1,\dotsc,M_n\...
3
votes
1answer
81 views
Detect non existence of a cycle in a graph using Datalog : SMTLIB Format for Z3
I want to detect the non existence of a cycle in a graph using Datalog (which is a declarative logic programming language).
The proposed solution was:
...
0
votes
0answers
25 views
Formula instead of predicate
A model is finite. How to replace an some predicate $P$ with a formula $\varphi$?
Example: $\{a, b, c\}$, $A = \{a, b\}$,
$\psi = (\exists P)((\exists x) (A(x) \wedge P(x)) \wedge ((\exists x) (A(x) ...
1
vote
0answers
44 views
Difference between logic, fuzzy logic, probabilistic logic, quantum logic?
I am not sure if the names of these logics are right, but I saw that you can generalize logic with probability theory. Then I found 3 ways of reasoning with probabilistic/smooth logic, Fuzzy, Bayes/...
2
votes
1answer
31 views
Finiteness of the set of equivalence classes of formulas generated by boolean combination
Define a relation $\equiv$ on the set of modal formulas by
$\phi \equiv \psi \Leftrightarrow (\forall M\forall w, M,w \models \phi\Leftrightarrow M,w \models \psi)$ (so it is an equivalence relation)
...
3
votes
1answer
63 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
52 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
76 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
24 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
30 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
75 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
29 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
48 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
61 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
40 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
169 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
27 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
99 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
47 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
14 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
20 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
681 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
71 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
46 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
47 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
121 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
33 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 ...
