Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
0
votes
1answer
14 views
List of all possible reasoning tasks - satisfiability and theorem proving only?
What is the exhaustive list of reasoning tasks? As far as I can understand, then any logical reasoning reduces to 2 tasks only: 1) satisfiability problem (finding the assignment of the variables) and ...
-1
votes
0answers
30 views
Is it there any hypothetical computer/hypercomputer model of the universe where logically impossible/illogical things could happen?
Trivialism is a system that proposes that literally every proposition is true and false at the same time blatantly breaking the principle of no contradiction and triggering the principle of explosion (...
0
votes
2answers
29 views
how do we demonstrate using Boolean algebra that these NAND and NOR gate combinations are XOR gates
How do we demonstrate using Boolean algebra that these NAND and NOR gate combinations are XOR gates?
1
vote
1answer
33 views
Are the two LTL properties $GF(\psi_1 \land F\psi_2 )$ and $GF(\psi_2 \land F\psi_1 )$ equivalent?
Is $GF(\psi_1 \land F\psi_2 )$ equivalent to the property $GF(\psi_2 \land F\psi_1 )$?
Attempt:
In the first property each state must eventually see $\psi_1$ and $\psi_2$, in the second property as ...
0
votes
0answers
51 views
Can hypercomputation compute the impossible? [on hold]
There are things which are illogical/logically impossible (like saying that 2+2=4 and 2+2=5. Without changing anything in the axioms of mathematics or logic, this would be a contradiction and would be ...
0
votes
1answer
20 views
Boolean expression for sum bit of full adder
The Boolean expression I find on the internet for the sum bit of a full adder is A xor B xor Cin. Does't this expression exclude the A=1,B=1,Cin=1 situation? When that happens, the sum bit is also 1, ...
0
votes
0answers
24 views
Algorithm to find possible variables in multiple connected equations
I am new here. I am trying to come up with an algorithm that can give me the unknown values in the following equation.
...
0
votes
0answers
26 views
Handling $AND$ and $OR$ cases in MILP?
Suppose I want to have an integer program for handling the cases
$x_1>1\wedge x_2>1\wedge x_3>1\wedge\dots\wedge x_n>1\iff\delta=1$
$x_1>1\vee x_2>1\vee x_3>1\vee\dots\vee x_n&...
0
votes
0answers
23 views
Hoare triple: Loop invariant and correctness
The following Hoare triple in which variable a is an array of integers, and len, max, i, n, j and m are integer-valued variables. Provide a loop invariant (using predicate logic) suitable for proving ...
2
votes
0answers
32 views
Hoare triple: Loop invariant and partial correctness
Below there is Hoare triple in which variable $a$ is an array of integers, $len$, $x, i$ are integer-valued variables, and $r$ is a Boolean-valued variable. I have to provide a loop invariant (using ...
2
votes
0answers
22 views
kPDA handling multiple epsilon transtions
I'm assigned to build a kPDA with 2 stacks that handles {w#w, where w is a string of (0,1)*}. I understand the # delineates the two strings, but I'm unsure of the logic when popping off stacks with ...
1
vote
2answers
74 views
What are the other language models of computation similar to lambda calculus?
I hope this question makes sense, but I was wondering if there are other models of computation similar to lambda calculus that you can use to build up axiomatic mathematical and logical fundamentals ...
5
votes
2answers
2k views
Why do ¬, ∀ and ∃ have the same precedence?
I thought the order of precedence of operators and quantifiers was arbitrary, but I don't really understand why those three have the same "strength" in relation to other operators (e.g., ¬ will have ...
1
vote
0answers
25 views
How do I get the NAND gate configuration for full adder from the logic table?
I'm self-studying, but I've gotten stuck already. If I'm given the logic table for a full-adder or any two-output table, how do I figure out the NAND-gate configuration, preferably methodically? ...
1
vote
0answers
26 views
Can we ignore the postcondition in the Hoare conditional rule when there is a return statement?
I'm proving the correctness of naive string matching using Hoare logic. I have the following pseudocode:
...
2
votes
1answer
58 views
Negation of the semantics of the Until operator in LTL
I have been looking at the Until operator and the release operator and when introduced to the release operator it was suggested that it is equivalent to:
$\phi R \psi \equiv \neg(\neg\phi U \neg \psi)...
1
vote
1answer
34 views
Turing Machine where branches are resolved via arbitrary operator
Alternating Turing Machines output Boolean values and combine the values returned by branches via the any/all operators. Is ...
1
vote
2answers
56 views
If a NAND gate is universal, why you don't have NAND OISCs
If a NAND gate can be used to construct all other of the basic logic gates, then I'm wondering why you don't/can't have a purely NAND-based One Instruction Set Computer (OISC). All the OISC single ...
0
votes
0answers
35 views
Can we see all of mathematics as an attempt to simplify computations?
This is a rather strong claim, and therefore likely to be incorrect, but hear me out.
Firstly, when I talk of “computations”, I mean this in a broader sense than normally used, because I am including ...
1
vote
2answers
38 views
(Generally) How to specify asynchronous action with side effects using logic equations
Say you have this function call sequence:
function all() {
fn1()
fn2()
fn3()
}
And say that fn2 was asynchronous and ...
2
votes
1answer
37 views
Examples of logic gates using non-standard models
These are the only ones I have been able to find online:
Pulley Logic Gates
Marble adding machine
MARBLE COMPUTER LOGICAL AND GATE
I would like to find some more discrete models like these (as ...
0
votes
1answer
25 views
LTL to Büchi automaton, deterministic?
I know it is possible to convert LTL formulas to Büchi automatons. But is it possible to convert a LTL formula to a deterministic Büchi automaton? Are there formulas that can't be converted to a ...
2
votes
1answer
17 views
How to understand the notion of boolean query via Immerman's definition
A query is any mapping $I:STRUC[\sigma] \to STRUC[\tau]$ that is polynomially bounded. A boolean query is a map $I_b: STRUC[\sigma] \to \{0,1\}$. A boolean query can also be thought as the susbset:
$...
3
votes
2answers
92 views
Interesting logic problems
I've just began a course on logic and learned the following :
De Morgan's laws
Normal forms
How to represent a logical formula (using or, and, not operators) using binary trees
How to ...
1
vote
2answers
75 views
D flip flop : How does it work in depth
I'm coming to you today because I have some trouble to understand how works D flip flop in depth. Two weeks ago we started at school learning sequential logic and so register and everything that come ...
5
votes
2answers
59 views
Topology vs sigma-algebra's as a framework for approximate information?
In the book "topology via logic" by Steven Vickers, topology is introduced for computer scientists, with the idea that topology captures the idea of approximate information.
I am somewhat confused ...
2
votes
1answer
150 views
Decidability of equivalence to existential formulas
I'm looking for an algorithm to decide if a given first order formula over a fixed vocabulary admits a logically equivalent existential one (i.e. a formula in prenex form where all quantifiers are ...
0
votes
1answer
42 views
How to evaluate dynamical conditioning/pseudo code
I am having a hard time even to formulate my question, so here it is:
I have an application that the user can go in and define on a webpage the logic one wants to evaluate for the student to comply ...
1
vote
1answer
45 views
What is the signature of a formal language?
I will briefly state the context where my doubts arise.
I know the following definitions.
A formal language is a set of well-formed formulas. It's a tuple constituited by an alphabet and a formal ...
0
votes
0answers
22 views
Can I use the Quine-McCluskey to simplify a CNF which is not a product of maxterms?
As I understand it the Quine-McCluskey method allows you to start with a set of maxterms (or minterms), and combine them pairwise in a systematic way into a smaller set of clauses with a smaller set ...
0
votes
0answers
13 views
KB implication vs and
i m doing KB from sentence to model.
I m stuck on this sentence that say this :
The packages stored in room1 are smaller than those stored in room 2.
I m created this vocabulary
Package X
...
2
votes
2answers
128 views
Absorption rule in Boolean algebra
I am confused regarding the absorption rule which states: A OR (A AND B) = A.
I do not completely understand how the expression simplifies to A and while i have seen proofs for this question, i still ...
1
vote
2answers
49 views
If you can represent/model a Conditional IF statement with AND + NOT or OR + NOT
I am still trying to wrap my head around this, which shows how to simulate control-flow without using an if-statement.
I've been looking at basic logic today and ...
0
votes
2answers
52 views
How “add” could be implemented in only bitshift operations
Typically, add/subtract/multiply/divide are primitive operations in an Instruction Set Architecture (ISA). I am interested to know if they can instead be implemented efficiently using only bitshift ...
1
vote
1answer
53 views
does the order of the rows matter? [closed]
from my understanding the truth table is supposed to generate every possible combination of true and false values without the order of the combination taking into account.
however one of my teachers ...
0
votes
2answers
33 views
Why we treat sentence letter $Q$ as conclusion in one form and premise in other?
Sorry for asking such a dumb question.
I am CS student and I am trying to understand the basic tenets of Logic. I am new to the subject and I am lost understanding Implication.
In formal logic, $(P\...
1
vote
0answers
18 views
Superposition calculus: greater vs greater-or-equal
Bachmair and Ganzinger 1991, 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', specifies the criterion for using an equation as, by some appropriate ordering, ...
1
vote
0answers
186 views
Could you show the intractibility of SAT by showing that the number of variables contributing to an arbitrary unsatisfied clause is not constant? [closed]
Preface: This is not an attempted proof at P vs NP
Starting with some CNF Boolean expression ϕ, by the rules of logical disjunction, a clause is only unsatisfied if each of the literals in it are ...
0
votes
1answer
32 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
45 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
1answer
25 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
42 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
21 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
41 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
31 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
31 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
43 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
29 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
115 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 \...
