Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
890
questions
0
votes
0answers
19 views
Need term to discriminate between inference rule and the rules in code that execute the inference rules
In creating a logic system in a programing language (Prolog) that uses rules of inference there are also rules (Prolog) needed to execute the rules of inference.
For example from Types and Programming ...
0
votes
1answer
31 views
How do logical and bitwise operators work on numbers? (e.g "2 and not 5")
====TLDR=============================================================
Curious about the behaviour of logical and bitwise logical operations on integers, i.e with
and...
0
votes
0answers
33 views
8-bit binary to bcd converter Verilog
We have been given task to write a 8-bit binary to bcd converter Verilog code, using structural code NOT behavioural, is it possible to guide us how can we create 8-bit binary to bcd converter using ...
3
votes
1answer
37 views
Stalmarck's method: x ≡ x → z, does z have to be true?
I have been researching Ståmarck's method 1. In the paper cited here, some rules are given. Rules are made of triplets (x, y, z) such that:
y $\to$ z $\equiv$ x
where x, y and z are booleans which ...
-1
votes
1answer
18 views
Conjuctive Normal Form
Let f(P,Q,R) be the truth-function defined as follows. f(P,Q,R)=1 if and only if
Q and R have different truth-values; or
P and R have the same truth-values.
Choose all formulas that are in conjunctive ...
2
votes
2answers
84 views
What if solving P vs NP revealed a contradiction?
Let's just say that some person discovered that $P = NP$ implies $P \neq NP$ and $P \neq NP$ implies $P = NP$, and we don't know what is causing this contradiction, And this was a valid proof that was ...
-1
votes
0answers
15 views
Is this depiction of dual 4x1 multiplier correct?
Please tell me if the logic behind table is correct and is the block diagram correct
-1
votes
0answers
60 views
Does the halting problem apply to a Dialetheistic logic(logic where a statement can be true, false or both) turing machine?
This hypothetical modification of a Turing machine would operate on balanced ternary, Dialetheist logic, which allows some controlled contradictions. In this logic a statement can have 3 values. False(...
2
votes
1answer
34 views
Resolution algorithm does not seem to generate the empty clause
Let's assume I have the following 3 clauses:
$\neg T$,$\neg Q$, ($\neg P \lor Q \lor S \lor T)$,$(\neg U, T, \neg S)$,$(\neg U, T, P)$
and I want to see if our KB entails $\neg U$ so I tried to apply ...
0
votes
0answers
56 views
Construct CFG of monadic logic
How to construct CFG for tautologies in monadic predicate logic in the empty model. The predicates are Q and P, operations are ...
2
votes
1answer
37 views
CTL trouble translating text into formula
I have an excercise where I have to translate verbally formulated statements into CTL formulas. I have particularly trouble with this one:
On every path q is true at least once and p was true ...
1
vote
0answers
15 views
Proving set of register machines that halt before k steps for some input is non-recursive
Given an enumeration of register machines $R_n$ that take a single natural number as input, and a constant $k$, the function $f$ is defined as:
$$
f(n) = \begin{cases} 1 & \exists m \text{ such ...
0
votes
0answers
26 views
Specific quantifier elimination for real algebraic numbers
It is well-known that the theory of (first-order) real arithmetic, $\mathcal{T}_{\mathbb{R}}$, is decidable, both on its linear and non-linear (a.k.a field) fragments, since Tarski-Seindenberg proved ...
1
vote
0answers
43 views
Automated theorem provers: limited by search heuristic?
My understanding of most automated theorem provers (which is possibly an incorrect understanding!) is that they start with some premises stored as unprocessed statements, and repeatedly select one to &...
3
votes
3answers
145 views
How many possible arithmetic operations are there between two N-bit numbers?
It's generally considered to be the case that there are sixteen possible logical operations between two N-bit numbers and four possible logical operations on one N-bit number. I'd like to know how ...
1
vote
0answers
42 views
Translating Natural Language to LTL Formulae
I'm brand new to LTL and working on becoming better with LTL formulae. I've got two examples where I am unsure whether my LTL formula is correct.
I'm given the sentences, and my assumption is that $l$ ...
0
votes
1answer
48 views
Domain of discourse vs First-order theory
In the question (Validity of predicate logic formulas) I see the following way of expressing:
"The predicate $P(x,y) \equiv \bigl[ y \cdot x = 1 \bigr]$, where the domain of discourse is $\...
0
votes
1answer
23 views
Determine if the following arithmetics are sentences
How would you determine if these arithmetics are sentences or not?
-(x + 2) > y
i++ == 2
i++ == 2 is this sentence True where i = 1
I understand it as if the ...
0
votes
1answer
30 views
Is it possible to encode contradictory horn clauses without goal clauses?
Intuitively, this seems impossible (because negation is forbidden in the head), but i am not sure.
A naive (and wrong) example is
p :- p
But, this just means
...
0
votes
1answer
65 views
How can we construct algorithm to evaluate logarithm of a real positive number
How can we construct the algorithm to evaluate the logarithm of a real positive number bit by bit in the base 2 system?
I have first expressed any number as $x\cdot2^n$, where $x \in [1,2]$, by ...
0
votes
0answers
92 views
Alu architecture of a Hack Computer
I'm currently studying the ALU architecture (of a Hack computer) and how it works.
As part of my assignments, I have been asked the following question:
If we want the ALU to compute the function y-1, ...
-1
votes
2answers
91 views
Proof of a logical theorem
Prove that if for every proposition $\psi\left(p_{0}, \ldots, p_{n}, p\right)$ there exists
$\phi\left(p_{0}, \ldots, p_{n}\right)$ in which $\psi\left(p_{0}, \ldots, p_{n}, p\right) \rightarrow\left(\...
0
votes
0answers
16 views
Method for minimizing relays in a switching/steering network - combinatorics/CSP algorithm exists?
This question is borne from the electrical engineering world, so I first asked it there, but it's really more of an algorithm optimization problem that everyone here might be better suited to help ...
0
votes
2answers
70 views
Validity of proof by contradiction
I had a doubt in the proof by contradiction technique.
Under this technique, we assume the negation of what we want to prove as true, then show that assuming so generates a contradiction. Since a ...
0
votes
1answer
66 views
Sorting by boolean algebra (hardware) instead of algorithm (software)
Consider there's an 5 elements list that foreach element are 2-bits. Forexample [01,00,10,00,11], if the list is sorted, we hope the output like this [00,00,01,10,11]
Maybe that case seems complicated,...
1
vote
0answers
38 views
"Universe-shrinking" function in Agda
Agda does not allow datatypes in one universe to be indexed by, or non-trivially parametrized by a type in a larger universe (strangely, Coq does not appear to require this for propositional ...
1
vote
1answer
71 views
To prove (KB ⊭ S) and (KB ⊭ ¬S) is satisfiable
In question (e), I have to prove: A ≡ (KB ⊭ S) and (KB ⊭ ¬S) is satisfiable, where KB and S are propositional variables. I am not able to follow the solution given in the image above as to why it is ...
0
votes
1answer
96 views
XOR gate from default-on/default-off relays, this simplest possible?
Playing nandgate to learn logical gates. Is the design below the simplest xor gate that can be built using the relays available? Seems like crossover relays allow a much simpler xor gate but don't ...
2
votes
2answers
105 views
Satisfiable CNFs where each clause contains logarithmically many different literals
Studying for my finals in Complexity theory. This question comes up in different variants and it requires to use probability.
A side note before, to be more clear: A CNF clause consists of $n$ clauses
...
3
votes
1answer
127 views
Why is it useful to transform 0-1 integer programming problem into SAT problem?
There are several researches studying translating 0-1 integer programming into CNF form. For example, this paper and this C++ library. As the lecture notes here goes, translating 0-1 integer ...
0
votes
0answers
36 views
Is there an alogrithm that analyses mistakes and increses weighting of a certain subject based on the mistake?
I am building a program that analyses a students mistakes and that mistake is linked to a topic. Then the program gets the information that a certain person has made x mistakes on some topic. I want ...
1
vote
1answer
89 views
Incomplete definition of function- first order logic
Let $\Sigma=\{c,f^1,R_1^2,...,R_k^2\}$ where $c$ is constant, $f$ is one argument function, and $R_i$ are binary relations.
Let $\Sigma_2=\{c',g^2,R_1'^1,...,R_k'^1\}$ where $c'$ is constant, $g$ is ...
2
votes
2answers
105 views
Problem with formalism in first order logic
This is a general question in first order logic.
Assume I have alphabet $\Sigma$ that contains one-argument function (among other symbols).
I want a new alphabet, $\Sigma'$, which is the same as the ...
2
votes
1answer
71 views
equivalence of validity above different alphabet
Given the next alphabets: $\,\,\Sigma_1=\{R^2,P^1,=^2\}\,\,,\Sigma_2=\{c,f^1,=^2\}.$
Prove of Disprove: There's exists an algorithm, that given formula $A$ above $\Sigma_2$, builds formula $A'$ above ...
1
vote
0answers
42 views
Herbrand universe with infinite terms (for a lazy programing language)
I am working with a toy programming language for my thesis. It is lazy evaluating so I can have infinite terms (for example the "infinite natural number" ...
2
votes
1answer
104 views
Proving that there are more problems than solutions
I have doubts regarding a proof of the following theorem:
'Set of all problems' is larger than the 'set of all algorithms' (or set of all C programs).
Put rhetorically, the theorem says that there are ...
2
votes
1answer
63 views
What are the limits of Boolean Algebra?
Any decision problem algorithm can be represented as a boolean expression. The rules of boolean algebra (De Morgan's law, distributivity, etc.) can be used to manipulate and simplify that expression, ...
3
votes
1answer
30 views
Is an AND gate which is noisy 1/3 of the time on only one of its inputs universal?
Imagine you have a noise-free NOT gate, and an AND gate with the usual truth table
00 0
01 0
10 0 (*)
11 1
but such that the case (*) is wrong 1/3 of the time, ...
0
votes
1answer
32 views
What Is the Currently-Known Simplest NOR-node Directed Cyclic Graph That Produces Pi?
Any directed graph (including a directed cyclic graph or DCG) has a complexity measure. We know that NOR is a universal logic gate, in the sense that a DCG whose nodes are n-input NOR gates can ...
0
votes
0answers
44 views
What is meant by A determine BC in functional dependency. How the validity of this statement will be checked
We use notation A determines BC in a database for functional dependency. Same way we use equations in mathematics which shows dependency of variables. We have inference rules in logics, functions in ...
0
votes
0answers
21 views
Software for proving tautology with steps
I'm looking for a software which can prove a tautology using logical equivalences.
It should be able to show each step. So you can follow the chain of reasoning.
Here is an example:
\begin{align}
(p\...
1
vote
2answers
253 views
Weird "proof" recursion
Assume we have some statement called $\alpha$. We will define a new statement $P(\alpha):="(\alpha\text{ can be proved})\lor(\lnot\alpha \text{ can be proved})"$
I claim that $P(P(\alpha))$ is always ...
0
votes
1answer
36 views
Is a Turing Machine a Well-formed formula?
Today i wrote something about the bijection between turing machines and recursive functions. And i describe a Turing Machine as a Well-formed formula because it seems like a WFF to me.
But is it ...
1
vote
1answer
69 views
Proving intuitionistic tautologies in Agda
I am to use Agda to prove some intuitionistic tautologies. One of them is the so called Weak Peirce's Law
$$
((((A \rightarrow B) \rightarrow A) \rightarrow A) \rightarrow B) \rightarrow B
$$
I ...
1
vote
0answers
41 views
What is the connection between finite automata and logic (sequential calculus)?
Languages recognized by finite automata are exactly those definable
by sentences of the sequential calculus, and also exactly those
definable by rational expressions (also called regular expressions)
...
1
vote
1answer
44 views
a conjunctive normal form that is a tautology
Are there any examples of CNF formulas that are tautologies?
Such that every clause contains different variables so phrases like (a or not a) are rejected?
0
votes
0answers
35 views
Please help me fix / finish this Fitch proof, I am stuck
Using the Fitch application and only Intro and Elim rules (& REIT if necessary), prove that
$$\forall x \forall y (P(x) \implies Q(y)) \iff (\exists x P(x) \implies \forall y Q(y))$$
is a logical ...
1
vote
0answers
21 views
Analogue of disjunction and existence properties for a Turing-complete programming language?
Quoting from Wikipedia:
In mathematical logic, the disjunction and existence properties are
the "hallmarks" of constructive theories such as Heyting arithmetic
and constructive set theories ...
0
votes
0answers
24 views
Hoare Triple Logic
I'm having trouble understanding the logic behind Hoare Triples. The question asks for the missing value of the precondition {X}
...
-2
votes
1answer
22 views
Are single complements the same as seperate complements?
Is (A' + B') the same as (A + B)' ?
Note: The apostrophe ( ' ) represents the complement
