Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

Filter by
Sorted by
Tagged with
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 \...
dalz's user avatar
  • 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 ...
JobHunter69's user avatar
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 ...
user1868607's user avatar
  • 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 ...
cozen's user avatar
  • 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 ...
Dylech30th's user avatar
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 ...
Andrew Baker's user avatar
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 (\...
ShyPerson's user avatar
  • 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 ...
Catherine H.'s user avatar
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 ...
Zaz's user avatar
  • 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 ...
phuck's user avatar
  • 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 ...
alim's user avatar
  • 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. ...
Weier's user avatar
  • 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 ...
ShyPerson's user avatar
  • 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?
Hovercraft2's user avatar
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$ ...
ShyPerson's user avatar
  • 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 ...
Motorhead's user avatar
  • 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 ...
Mikayla Eckel Cifrese's user avatar
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 ...
Jonas's user avatar
  • 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 ...
aweeeezy's user avatar
  • 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 ...
Nav's user avatar
  • 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'...
Michal Dvořák's user avatar
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 ...
Daniel's user avatar
  • 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 ...
asha soroushpoor's user avatar
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 ...
Soha's user avatar
  • 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 ...
manu fava's user avatar
  • 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 "...
Jonas's user avatar
  • 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 ...
geofflittle's user avatar
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 ...
Angelo's user avatar
  • 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$...
G S's user avatar
  • 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 ...
Zoha Javed's user avatar
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 ...
dgan's user avatar
  • 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 ...
Jip Helsen's user avatar
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....
FirePapaya's user avatar
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 ...
aome's user avatar
  • 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 ...
Ank i zle's user avatar
  • 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 ...
Tita's user avatar
  • 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 ...
Jean-Baptiste's user avatar
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 ...
mrak-p's user avatar
  • 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 ...
jack malkovick's user avatar
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. ...
Danila Nikolaychuk's user avatar
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....
lafinur's user avatar
  • 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 ...
FrogOfJuly's user avatar
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 ...
user49413's user avatar
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 ...
user avatar
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 ...
user avatar
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,...
J. Schmidt's user avatar
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 ...
siv2r's user avatar
  • 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 ...
infinicky's user avatar
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 ...
Motorhead's user avatar
  • 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 ...
Hank Igoe's user avatar
  • 179

1
2 3 4 5
20