Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
0
votes
1answer
19 views
Can you connect an output from a logic gate to 2 or more logic gates or inputs?
I have been given this diagram of a circuit:
https://www.google.com/search?q=full+adder+logic+gate&rlz=1C1CHBF_enCA831CA831&source=lnms&tbm=isch&sa=X&ved=...
0
votes
1answer
22 views
Simplifying SOP: implementing OR with NAND
I am learning how to implement basic logic gates using NAND. I have learnt that you can use De Morgan's theorem as such:
$a+b = \bar{\bar a} + \bar{\bar b} = \overline{(\bar a *\bar b)}$
In other ...
0
votes
0answers
11 views
Superposition calculus: Elimination of redundant atoms
Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', section 5.2, 'Simplification and Deletion Techniques', page 17, 'Elimination of redundant ...
2
votes
1answer
33 views
Reasoning about resources: “resource logics”?
Are there extensions of predicate logic which focus on resource models, possibly even in actor models?
And if so, would it be possible to reason on a meta-level on how many resources should be ...
1
vote
1answer
20 views
Bachmair and Ganzinger, ordering of equations
Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', page 4, defines an order on equations. (This is an arcane piece of machinery but a critical ...
0
votes
1answer
40 views
Find value of $a$ or $b$ of two XOR equations
Is it possible to find $a$ or $b$ given that $a \oplus b = c$ and $c \oplus b = a$ when I only have the value of $b$?
0
votes
1answer
34 views
How to “logically” solve boolean logic
I came across of one excellent book Elements of Computing Systems and in chapter 1 we need to implement the "primitive" logic gates (for example: Not, And, Or, Xor, Mux, etc) based on a Nand gate.
...
1
vote
1answer
25 views
Check if one condition includes another
I have two conditions A and B in a form of "ast tree".
How can I check that B is more strict than A?
I.e. if B is true then A is always true.
Example
A:
x = 1 and (b = 2 or c = d)
B:
y = 5 and x = ...
1
vote
0answers
23 views
Why Modus ponens works with Horn clauses and Generalized Modus ponens requires definite clauses?
I am reading the Artificial Intelligence: A Modern Approach book and in the chapters about logic i noticed that in propositional logic the Modus ponens inference rule (used by the forward and backward ...
1
vote
1answer
37 views
Validity of CTL formula $s_0 \models EG\ AF\ p$ in given model
I have been learning Verification by model checking recently and I get the following question:
Is the CTL formula $s_{0} \models EG\ AF\ p$ valid in the following model?
I think it is ...
1
vote
1answer
14 views
How to prove a LTL formula correct in a specific model?
I have been learning Verification by model checking recently and I get the following question:
$Whether\ the\ LTL\ formula\ M, q_3\ \models (X\ \lnot a) \rightarrow (F\ G\ \lnot a)\ is\ established\ ...
0
votes
1answer
91 views
Can this set of propositions be represented and proved in Haskell?
I used a set of natural language statements and their formalization from Gries and Schneider. I attempted to transform the propositions into Haskell equations. For example, for S0 : $a \land w \...
3
votes
0answers
17 views
conversion of basic $\text{CTL}^*$ formulas to $\text{CTL}$
Consider the $\text{CTL}^*$ formula $E[pU(qUr)]$.
It is not hard to show that it is equivalent to the $\text{CTL}$ formula $E[pU(EqUr)]$.
The informal reason is that a path where $p$ is true until $...
1
vote
2answers
64 views
Must $x$ and $y$ be different in a statement of the form $\forall x \forall y \cdots$?
Given the following predicate formula $F$:
$$\forall x \forall y [(\text{italian}(x) \Rightarrow (\text{winWC}(y) \Rightarrow \text{happy}(x))]$$
I am having trouble understanding whether $x$ and $y$...
3
votes
1answer
61 views
Roadmap to formal verification
I would like to learn about different approaches to formal verification of software programs that goes beyond what Wikipedia has to offer. Ideally one would not only get an overview but also ...
1
vote
2answers
66 views
Validity of □(P→ Q) → (◊P → ◊Q) in linear temporal logic
How can I prove that $\Box(P\rightarrow Q)\rightarrow (\Diamond P\rightarrow\Diamond Q)$ is valid in linear temporal logic (LTL)?
0
votes
0answers
31 views
Turing machine, tape without blanks, does it halt or no?
So I'm lost on this one. We're given a turing machine and an initial tape. Tape is infinitely long in both ways, but all the blanks are taken out. The head is the leftmost nonblank. So the question is:...
0
votes
0answers
9 views
Timed Kripke structures with inequality constraints
I am having problems creating a timed Kripke structure $\mathcal{TK} = \langle S, \mathcal{T}, \rightarrow, L \rangle$ for a system that I have.
My system, a timed automaton system (time base $\...
1
vote
0answers
22 views
Unification algorithm that directly finds multiple substitutions?
Systems of formal logic generally have inference rules that
require certain expressions to be syntactically the same
in multiple steps. Typically two steps are involved, as
for modus ponens, where ...
1
vote
3answers
88 views
Soundness and completeness w.r.t. programming languages
I'm studying programming languages (more specifically type systems) and came across a concept I couldn't quite wrap my head around: soundness and completeness.
I'm taking a class, and according to my ...
0
votes
1answer
36 views
Finding CNF of $(p \rightarrow q) \rightarrow p$ and $\lnot (q \wedge (\lnot p \rightarrow q)) $
I'm trying to find the CNF of the $(p \rightarrow q) \rightarrow p$ and $\lnot (q \wedge (\lnot p \rightarrow q))$, and afterwards proving it's validity. As i'm new to CNF i wanted to ensure i've ...
1
vote
1answer
35 views
predicate logic proof of 2 numbers
For any two different numbers there is an number in between.
I'm trying to write this in predicate logic and have no idea how to do it, since I need 2 variables X and Y? For all x there exists a y ...
-1
votes
1answer
26 views
predicate logic/binary relation help
(1) ∀x, y, z (x < y ∧ y < z → x < z) (transitivity)
(2) ∀x ¬(x < x) (antisymmetry)
(3) ∀x, y (x < y ∨ x = y ∨ y < x) (linearity)
I need to give an example of a (nonempty) ...
0
votes
0answers
8 views
Determining the max frequency of a cycle with flip flops
The following cycle is given and i need to determine what is the max frequency possible for it.
The cycle has 3 positive D-edge Flip Flops and some logic gates.
i calculated the time it takes for ...
0
votes
1answer
32 views
Would hypercomputation machines be capable of simulating/computing/programming everything?
If uncomputable numbers existed, could this hypercomputation machines compute them? Could hypercomputation compute all types of uncomputable things? Even truly inconsistent things? Even things that ...
3
votes
2answers
69 views
How could a formal system ever be non-obviously unsound?
When reading discussions of Gödel's theorems one is always heeded that just because formal system $F$ proves a theorem $T$ that doesn't necessarily mean that when one applies the intended ...
0
votes
1answer
24 views
Determining cycle time and and hold time in logic circuits
First I have general question. In a circuit with both logic and D edge flip flop does hold time have to satisfy $t_{hold} < t_{setup}($D-FF$) + t_{pd-min}$(Logic),
or is it enough that $t_{hold} \...
0
votes
0answers
21 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 ...
1
vote
0answers
16 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
27 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 ...
1
vote
0answers
28 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
56 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
2answers
120 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
104 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
26 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
29 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
16 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
39 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
1answer
25 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
85 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
58 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
62 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
68 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
72 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 ...
13
votes
1answer
278 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
41 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
86 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:
...
1
vote
0answers
59 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/...
3
votes
0answers
49 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)
...
