Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
980
questions
1
vote
1
answer
36
views
(Co)-induction, fixpoints and inference systems
I'm learning about induction and co-induction. From what I know, given a set of judgments $U$ and an inference system $\Phi \subseteq \wp(U) \times U$, where $(\left\{ h_1,\dots,h_n \right\}, c) \in \...
- 13
1
vote
0
answers
19
views
How do I prove relations of two CTL formulas?
If I have two CTL equations, how do I prove they're equivalent or that one implies the other?
What's the general approach? Disproving is obvious, but I am unable to figure out how to prove the ...
- 121
1
vote
2
answers
57
views
Complexity of satisfiability for relational logic on the booleans
I know that propositional satisfiability is NP-complete and that if I add first-order quantifiers I get the complete problems for the polynomial hierarchy and PSPACE. What happens if my formulas are ...
- 2,184
0
votes
2
answers
49
views
Is there a model for the given logical formula, and if not, why?
I'm trying to determine whether there exists a model for the following logical formula: $(p_1 \to (p_2 \lor p_3)) \land(p_2 \to \neg p_3) \land ((p_1 \lor p_3) \to \neg p_2)$. Here's my understanding ...
- 3
4
votes
3
answers
624
views
What is practically preventing us from applying set-theoretic types in engineering?
I know the title is sort of misleading because we do have set-theoretic types in several languages:) From a theoretic view, set-theoretic types such as intersection, union, and negation may bring some ...
- 41
6
votes
1
answer
707
views
Representing binary functions with a finite gate set without exponential blow-up?
It is pretty well taught that any binary function can be represented using CNF. But conversion to CNF can take an exponential number of gates. The truth table is exponentially sized relative to the ...
- 327
0
votes
1
answer
31
views
How big is a formula equivalent to a wff over $n$ variables with $2^n$ subformulas?
Definitions: Let $n \in \mathbb{N}$. If $\alpha$
and $\beta$ are propositional formulas,
then we'll call $\alpha$ and $\beta$ independent if neither implies the other,
or more formally, if $\lnot (\...
- 923
1
vote
1
answer
58
views
DFA for even concatenation of strings from a language
If I have a deterministic finite automaton (DFA) with a language $W$, and I need to create another DFA that returns all the strings that are a concatenation of an even number of strings in $W$, how ...
- 11
1
vote
0
answers
32
views
How to prove a minimum number of queries needed to determine a piece of information
You have 27 coins, 1 of which is a different weight. Using a balance scale with 2 pans, how can you determine which coin is different in only 4 weighings?
Generalize this to N coins.
Hint
Solution
...
- 111
0
votes
0
answers
26
views
Prove with natural deduction
Prove P ∨ Q, Q ∨ R, P → ¬R |- Q with natural deduction.
P ∨ Q, premiss
Q ∨ R, premiss
P → ¬R, premiss
...
...
Conclusion, Q
I dont know how to properly solve this question?
I know somewhat how to ...
- 1
3
votes
1
answer
167
views
how to do incremental construction of the minimal model in logic programming?
I was reading a book titled "Essentials of Logic Programming.", most parts of the book are easy to understand. but now having a problem with Theme 45: incremental constructions of the ...
- 984
5
votes
4
answers
876
views
Curry-Howard isomorphism and non-constructive logic
My understanding of the Curry–Howard correspondence is that it shows an isomorphism between constructive logic (also called intuitionistic logic) and computer programs in appropriate typed languages.
...
- 181
0
votes
0
answers
32
views
Growth of a set of propositional formulas under partial evaluation
Definitions: Let $n \in \mathbb{N}, n \geq 1$. We write $|\alpha|$ to denote the length in characters of an expression $\alpha$ in propositional logic. We define partial evaluation in the normal way ...
- 923
0
votes
3
answers
82
views
Is there a 2SAT encoding for a NAND gate
I am trying to encode some circuit checking algorithms, but encountered difficulty creating a 2SAT representation for a NAND circuit. Is there a proof that this is not possible?
1
vote
1
answer
36
views
Complexity of a Set of Formulas
Notation: We write $|\alpha|$ to denote the length in characters of an expression $\alpha$ in propositional logic.
Consider an expression $\alpha_n$ in disjunctive normal form built from $2n$ ...
- 923
0
votes
1
answer
36
views
Are recursive Horn clauses first order?
My understanding is that recursive definitions are considered second-order since they require the fixpoint operator in order to be formulated as "true" definitions. This is even though they ...
- 272
2
votes
3
answers
286
views
Does the first incompleteness theorem imply that any Turing complete programming language must have undefined behavior?
If I understand correctly, the first incompleteness theorem says that any "effectively axiomatized" formal system which is consistent must contain theorems which are independent of the ...
0
votes
1
answer
49
views
Could there be a computer or components based on a non-classical logic?
Since circuits and processors are heavily influenced and designed based upon boolean logic, which is itself a subset of propositional logic, could there be different interpretations of hardware or ...
- 103
0
votes
0
answers
33
views
Given a population, find the boolean algebra expressions that most closely evaluate to that population
TL;DR
I have some ideas but am curious to know if there are existing proofs, research, etc. in this area that I can use to guide my algorithm development.
Problem summary
We have a population where ...
- 101
-2
votes
1
answer
27
views
Equivalent logical statements confusion
First time posting here. If we have the logical statement ($A$ and $B$) $\rightarrow$ $C$ ($1$), we know that it is equivalent to ($A$ and $B$) $\rightarrow$ ($C$ and $A$) ($2$). Therefore if we ...
- 101
1
vote
1
answer
46
views
How to express that a graph has Independent set of size at least $n/2$ in $\exists SO$
I am looking to provide a formula saying "A graph with $n$ vertices has an independent set $X$ of size at least $n/2$" in existentional second order logic.
(This is exercise 1.2. from Libkin'...
- 267
0
votes
0
answers
30
views
Worst Case Response Time (WCRT) analysis the only necessary test for real time tasks?
Recently, I have taken a Computer Science exam for the course Operating Systems. One question was as follows:
Which statements about real-time operating systems are true?
I selected two options, but ...
- 1
0
votes
1
answer
42
views
Defining 2 inductive propositions relying on each other in Coq
I'm pretty beginner in Coq. I want to formalize negative and positive occurrence of an atom in a proposition inside coq the definition is as down below:
I want to define this property as an Inductive ...
1
vote
0
answers
30
views
Shortest unsatisfiable 3-CNF that can't be refuted with narrow resolution?
Proof width (the size of the largest clause in a proof) plays an important part in refuting an unsatisfiable formula. If a formula has a bounded-width resolution proof of its unsatisfiability, then ...
- 25
0
votes
1
answer
71
views
Relation between Curry-Howard isomorphism and Kripke semantics for intuitionistic logic
Intuitionistic logic(s) are usually defined in a purely synthetic way, with their own deduction rules different from classical logic, but they also have semantic interpretations.
One of them, more ...
- 101
0
votes
0
answers
31
views
What are the applications of Belief Revision?
In my Computer Science graduation, I came across this concept of Belief Revision, which focus on knowledge representation and the possible operations that can be done with the facts that a "...
- 103
0
votes
0
answers
37
views
Data structure for arithmetic logical queries
Abstract Problem
I'm looking for a data structure that will (1) allow me to make queries of the form A.x - B.x <= 0.1 AND A.y + B.y >= C.y + D.y and (2) allow ...
- 161
0
votes
0
answers
22
views
SOP Boolean expression of state variable and output of a Moore FSM
Disclaimer: I'm studying for an exam, but I don't have to hand in anything.
I have the state transition diagram of the FSM and its states encoding:
I want to find the sum-of-products (SOP) Boolean ...
- 1
1
vote
1
answer
44
views
Why do simple Logical Gates have an Irrational amount of Bits?
Suppose $2$ bits are used to encode a message, A and B.
If you know $A$ is $1$, you have one bit of information.
If you know $A\land B$ is $1$, you have two bits of information.
If you know $A\land B$...
- 13
0
votes
0
answers
50
views
Removing null production from cfg
While removing null production from cfg as below,
S->ABC
A->aA|^
B->bB|^
C->aaC|^
now as shown above we know that A,B and C all are ...
2
votes
1
answer
25
views
Sequent calculus and vs comma: $a \land b \implies ...$ vs $a, b \implies ...$
I was reading "Open Logic book", "Sequent Calculus".
Given the fact that all antecedents must hold for at least one succedent to hold, I can't get rid off the impression that using ...
- 123
-1
votes
1
answer
78
views
SAT polynomial time
Hi I understood it is not currently possible to solve SAT in polynomial time. Does this mean we can not currently solve an expression with n different boolean variables or with m different symbols in ...
- 103
0
votes
1
answer
51
views
Is any 2-CNF has 2-DNF representation?
I was asked a question whether I could come up with a 2-CNF over several variables that has no 2-DNF representation. However I thought that any CNF can be converted to DNF through some manipulations e....
- 103
0
votes
0
answers
49
views
How to efficiently recalculate iterative weighted center
I'm trying to write a gradient ascent approach to divide all points on a polygon into two sets via a continuous line (something like the below, where our polygon is a circle and we partition such that ...
- 101
2
votes
1
answer
60
views
Is finding a Polytime reduction from $L_1$ to $L_2$ equivalent to proving $L_2 \in P \Rightarrow L_1 \in P$
I often hear NP-completeness as problems such that, if they were in $P$ all problems in $NP$ are in $P$. The true definition, though, is that NP-complete is a set of languages in NP that all languages ...
- 153
0
votes
0
answers
59
views
Proving that the polish notation has unique readability
I am familiar with the polish notation when it comes to algorithmically reading phrases, but I am having a hard time proving the following exercise:
K is a function so that 1) $K(*)$ is an integer if ...
- 225
1
vote
0
answers
57
views
How do you deal with Skolem functions which escape their scope in elimination rules?
If you have an elimination rule for tuples which introduce the left and right pair into the type checking context, what do you do if the type of one of the elements is quantified and has been ...
1
vote
3
answers
112
views
How do you write a logic function to determine if one 2s complement binary number is less than another?
Working on logic design in class, and I'm trying to figure out how to write a specific logic function [and by write, I mean something along the lines of (x NOR y) OR (a NOR b), for example]
It asks to ...
- 11
1
vote
2
answers
59
views
What is the Kripke semantic for a linear temporal logic?
I've read that in general for a modal formula P, a world w and a Kripke frame ⟨W,R⟩
w⊨□P if and only if for every u∈W, if wRu then u⊢P
In case of LTL, being a modal logic, I assumed that the worlds ...
- 251
0
votes
0
answers
37
views
How to make a GUI for first-order logic representation?
This idea blows my mind, I would appreciate for any guidance. In essence, the question is how a machine should work to transform any kind of formal logic into its graphical representation (e.g. ...
1
vote
0
answers
48
views
Application of a formal definition of $max, min$ to evaluate an expression
For an Algorithms course we are studying propositional calculus. As an excercise we are given formal statements which we are to explain in natural language first and then evaluate with specific values....
- 181
2
votes
1
answer
53
views
What is the difference in heap configurations? Separation logic with CVC5 SMT solver
I am figuring out separation logic and trying to run simple examples in CVC5 smt solver. I am missing some core understanding of how pointers and values are treated there and I don't know where to ...
- 123
0
votes
1
answer
81
views
Can we accept that all axioms are equivalent?
The proposirional logic is based on 3 schema of axioms of which (A1) is
B ⇒ (C ⇒ B). Then, for any 2 axioms p and q, p ⇒ (q ⇒ p) is an instance axiom of (A1). We can have q ⇒ p by a step of MP as we ...
- 21
0
votes
1
answer
52
views
How to find a term that proves a given proposition?
I'm reading this book, and there's something basic that I don't exactly get. The authors say that every common noun is declared to be a type. For example, $Human:Type$. Then, they give an example of ...
user157472
1
vote
1
answer
44
views
Finding an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$
Let $\ast$ stand for "type" and $\square$ stand for "kind" so that $\ast:\square$. Suppose I want to find an inhabitant of $\Pi x: A.\Pi y:B(x). \ast$. The derivation rules are ...
user157472
2
votes
1
answer
38
views
What is the proper way to write logic formula, say concerning graph theory?
Say for example I'd like to state that there exists a pair of vertices such that they form an edge in one graph but not some other graph. I'd go about it as follows:
$$ \exists u, v \in V, (u,v) \in G,...
- 737
0
votes
1
answer
120
views
Is "Bitwise Complement Operator" (~ tilde) distributive?
To be more precise, Is ~(a+b) = ~a + ~b? Here, "~" bitwise NOT operator.
I ran into this question while thinking about ...
- 1
0
votes
1
answer
35
views
Logic for Computer Science - How to define msort, merge and split functions inductively?
In "Modelling Computing Systems: Mathematics for Computer Science", I came across a logic exercise to inductively define a merge sort function 'mergeSort', with a hint to first define ...
0
votes
0
answers
52
views
Constrained Horn Clauses vs. "ordinary" Horn Clauses
I see why ordinary Horn clauses (of the type Prolog might accept) are first order eg something like (with all variables universally quantified)
$$
P(x) \leftarrow Q_1(x),Q_2(x,y).\\
P(x) \leftarrow ...
- 272
1
vote
1
answer
50
views
K in SKI combinator calculus: why doesn't it take one parameter since it ignores its second?
In the SKI combinator calculus, Kxy returns the constant function which always returns x. Since y is always ignored, why not just define K as having a single parameter, namely, x? What is the purpose ...
- 179