Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

Filter by
Sorted by
Tagged with
2 votes
0 answers
45 views

Can remainder mod 2 be efficiently computed from addition and equality?

Suppose I have a programming language all of whose variables have natural number type. (So I cannot form higher-type objects, e.g., lists or trees, of natural numbers.) The only atomic commands I am ...
Siddharth's user avatar
  • 121
-1 votes
0 answers
11 views

How to extract Geo880 and Jobs640 dataset? [closed]

The links to both datasets are below: https://www.cs.utexas.edu/~ml/nldata/jobquery.html https://www.cs.utexas.edu/users/ml/nldata/geoquery.html I attempted to download them via FTP, but I can't ...
michael chen's user avatar
3 votes
1 answer
590 views

Can the minimisation operation be seen from a programming language perspective?

If $f$ is a total function $\mathbb N^k\to\mathbb N$, and $g$ is a total function $\mathbb N^{k+2}\to\mathbb N$, then we say that $h:\mathbb N^{k+1}\to\mathbb N$ is definable by primitive recursion ...
Joe's user avatar
  • 133
0 votes
0 answers
32 views

How can I know the complexity of my conceptual game and solving it with an algorithm?

I made a really simple card game where you and your opponent have 6 cards and in a turn you can use only one of them and it will be discarded. The cards have a value and an effect. The cards, with ...
michaelprimo's user avatar
1 vote
0 answers
33 views

Analog of semantic paradoxes in type theory?

By semantic paradoxes, I mean like the Liar paradox, Curry paradox, Knower paradox, etc. In classical (logic) settings, we would need to extend the language with a predicate P (truth or is-known ...
confusedcius's user avatar
1 vote
0 answers
25 views

How could higher-order Datalog be more expressive than first-order Datalog?

According to this paper [1], higher-order Datalog is more expressive: ... we demonstrate that on ordered databases, for all k ≥ 2, ...
MWB's user avatar
  • 505
0 votes
1 answer
59 views

P=NP? A reduction of CNF boolean satisfiability to the circulation problem in an undirected graph

The picture below shows how to reduce the Boolean Satisfiability problem in CNF to the circulation problem in undirected graph (see here). As you can see, a[i] are ...
Serge Rogatch's user avatar
1 vote
2 answers
33 views

Can a Code Script be Optimized for Time and Space Complexity Using Logic Gates

let's say that I have a Python script that performs various operations, including data manipulation, conditional logic, and iteration. However, I'm concerned about its time and space complexity ...
edge selcuk's user avatar
4 votes
0 answers
70 views

Extending Fagin's Theorem to the Polynomial Hierarchy

Fagin's Theorem (see Wikipedia and these lecture notes) states that there is an equivalence between second-order logic (SOL) formulas with existential quantifiers, and problems in NP. I was wondering ...
UserA2000's user avatar
0 votes
0 answers
27 views

Page miss in 2Q Cache Replacement

I am studying about 2Q Cache Replacement Policy and i came across this post. They have worked out an example with the following page keys [1, 2, 3, 4, 1, 2, 5, 1, 2, 3, 4, 5] and cache memory of 5 ...
user avatar
1 vote
0 answers
59 views

Prove or disprove that the Quine-McCluskey method generates the circuit with the minimum inputs and minimum gates?

Recently, when I self-learnt Discrete Mathematics and Its Applications 8th by Kenneth Rosen, it says in 12.4 Minimization of Circuits which uses the Karnaugh Map or the Quine-McCluskey method: ...
An5Drama's user avatar
  • 193
0 votes
0 answers
45 views

Do these courses fall under theoretical computer ccience [duplicate]

I am planning to apply for master's degree at TU Berlin and have to take some courses on theoretical computer science since the university requires me to take some credits on theoretical computer ...
Burak's user avatar
  • 1
0 votes
0 answers
43 views

Do these courses fall under theoretical computer ccience

I am planning to apply for master's degree at TU Berlin and have to take some courses on theoretical computer science since the university requires me to take some credits on theoretical computer ...
Burak's user avatar
  • 1
0 votes
0 answers
22 views

Do these courses fall under theoretical computer ccience [duplicate]

I am planning to apply for master's degree at TU Berlin and have to take some courses on theoretical computer science since the university requires me to take some credits on theoretical computer ...
Burak's user avatar
  • 1
0 votes
0 answers
15 views

Finding program that enumerates a language using Von Neumman's computability paradigm

Given an alphabet $\Sigma$ of $n$ elements, whenever there is some order $\leq$ over the elements of $\Sigma$, we define $s^{\leq} : \Sigma^{*} \mapsto \Sigma^{*}$ as \begin{align*} s^{\leq} \left(...
lafinur's user avatar
  • 181
4 votes
1 answer
191 views

SAT formulation of the condition that an even number of a given set of variables must be set to true

Lets say I have a SAT problem with variables $x_1,...,x_n$. For a given subset of the variables I want to create a clause which forces an even number of the variables in $S$ to be true. Of course ...
Sander's user avatar
  • 203
1 vote
0 answers
50 views

Is it known, whether the complement of NP-hard problems is necessarily again NP-hard?

Neither could I find any counterexamples, nor could I show that if indeed the complement of NP-hard problems was NP-hard, one could deduce some unknown results from it, which would imply that it is ...
LostBetweenTheLines's user avatar
1 vote
0 answers
34 views

What logical system does hindley-milner correspond to, according to the curry howard correspondence?

If I understand CHC correctly, simply typed lambda calculus corresponds to propositional logic. As HM allows polymorphic definitions by let-expressions, my guess is that it would correspond to a ...
pgmcr's user avatar
  • 36
1 vote
2 answers
52 views

What is "the ability of classical control operators to return multiple times from a single term"?

I am puzzled by a point in this paper by Phil Wadler. Figure 6 shows a proof of the law of the excluded middle, $A ∨ ¬A$. The computational interpretation of this proof exploits the ability of ...
Theo H's user avatar
  • 321
0 votes
0 answers
30 views

Expressing Boolean Functions In Terms of Another Function

Given two boolean functions f1 and f2, are there any tools available that could be used to automate the process to represent f1 in terms of f2? I understand the process of this doing this by hand ...
rotatinglemur's user avatar
1 vote
1 answer
113 views

Hoare Logic: Identifying Hoare Triple given a simple function

The program is designed to start with values for $x$ and $y$. The variables $u1$​ and $u2$​ are intended to represent $x$ and $y$ in ascending order. Provide suitable preconditions and postconditions ...
User's user avatar
  • 11
0 votes
0 answers
28 views

Karp-reduction of Disk Covering Problem

While preparing for final exam, I encountered a (target) problem where you have $M$ lines and $L$ points and you want to answer if it's possible to cover them all using $K$ disks of unit radius (...
pcko1's user avatar
  • 115
1 vote
1 answer
45 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
29 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
59 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,194
0 votes
2 answers
56 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
670 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
709 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
39 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
  • 925
1 vote
1 answer
71 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
36 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
  • 145
0 votes
0 answers
29 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
170 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
  • 1,004
5 votes
4 answers
958 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
  • 231
0 votes
0 answers
37 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
  • 925
0 votes
3 answers
85 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
39 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
  • 925
0 votes
1 answer
48 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
  • 282
2 votes
3 answers
323 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
53 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
2 votes
1 answer
63 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
35 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
53 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
36 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
3 votes
2 answers
97 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
  • 131
0 votes
0 answers
39 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
38 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
34 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 ...
sansarc's user avatar

1
2 3 4 5
21