Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

Filter by
Sorted by
Tagged with
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

1
2 3 4 5
18