Questions tagged [logic]
Questions related to mathematical logic and its use in computer science
821
questions
0
votes
0answers
11 views
Factor-graph formula
We know that we can break a normal function $g$ in the following way:
$$g(X_1, ..., X_n) = \Pi_if_i(S_i)$$
where $S_i \subseteq \{X_1, .. X_n\}$.
Now let's look at $g$ as a graph with the vertex set $\...
0
votes
1answer
20 views
Which of these properties hold for all FO theories? (but not regarding fragments thereof)
Which of these properties hold for all FO theories? (but not regarding fragments thereof)
a. Decidable
b. At least expressive as propositional logic
c. NP-complete
a) Decidable: no, some first order ...
-3
votes
0answers
21 views
SQL Error in my project
I have an issue with my project that I can not seem to solve.
I have tested for errors and can not seem to solve it.
Can someone point me in the right direction so that I can carry on with my project. ...
1
vote
0answers
17 views
Translating CTL into $\mu$-calculus
I have been studying $\mu$-calculus and right now I'm trying to translate CTL (computation tree logic) to $\mu$-calculus. I have found this article: https://www.win.tue.nl/~jfg/articles/CSR-10-09.pdf ....
0
votes
1answer
24 views
Create an Finite Deterministic Automata for a regular expression
I want to create a finite state machine that accepts the following language:
$$
L=\{w\in\{a,b\}^* | w \text{ contains abb but not on the first position}\}
$$
So I began by writing a regular expression ...
0
votes
1answer
28 views
Is Conjunctive Normal Form or not?
I have one formula that I do not understand why it is CNF and one that is not CNF, namely.
p && !q (NOT NCF)
and
!!p(CNF).
According to the exercise where I found these examples, 1 is not ...
0
votes
0answers
17 views
Is my UML Use Case Diagram valid?
I'm preparing an UML use case diagram for my following school project:
...
1
vote
0answers
33 views
Help me understand whether these critical pairs are joinable
I have the following TRS $R$:
$$
l_1 = f(g(x)) \to f(x) = r_1 \\
l_2 = g(f(y)) \to g(y) = r_2
$$
I want to know if $R$ is confluent, and whether $g(f(f(x))) \leftrightarrow_R^* g(g(g(x)))$.
I have ...
1
vote
0answers
48 views
Why is most research in logic and verification conducted in Europe rather than the US?
This is the CSRankings output for logic and formal verification for the last 10 years, worldwide:
http://csrankings.org/#/index?log&world
For the International Conference on Computer Aided ...
0
votes
0answers
9 views
How to combine multiple Boolean Functions in CDNF efficiently for implementation on a CPU?
I am trying to see how fast I can implement a 6-bits to 6-bites lookup table. Generally, I am attempting to do this by using the common method mentioned in CS textbooks of using the Quine-McCluskey ...
0
votes
0answers
17 views
Prove the boolean function E = F + G contains of the sum of the minterms of F and G
I'm given a boolean function E which is result of the sum of F and G (Where both F and G are boolean functions for sure).
By using K-Map I can easily understand why E would have the sum of the ...
0
votes
1answer
30 views
is duality principle in boolean algebra is true for every expression
Let say A = 1 and B = 1
and then A+B = 1
now by using duality(replacing or gate by and gate and 1 by 0) we can say that, A.B = 0
but this is not 0, because 1.1 = 1, so please anyone clear my ...
2
votes
0answers
20 views
Automated algorithm design
There is a huge field of study dedicated to automated theorem proving. Is there any similar research dedicated to automated algorithm design? And is there any form of "duality" between these ...
0
votes
0answers
28 views
Check if given safety properties are regular, and if so construct NFAs
Let $\mathit{AP} = \{a, b, c\}$. Consider the following LT properties:
Between two neighboring occurrences of $a$, $b$ always holds.
Between two neighboring occurrences of $a$, $b$ occurs more often ...
1
vote
0answers
29 views
Name for a function on formulae that does not break the structure of given formula
I have two logics, $L_1$ and $L_2$, and a mapping $f: Formulas_{L1} \rightarrow Formulas_{L2}$, and want to argue that the mapping is "nice", in the sense that it is structure-preserving. ...
4
votes
0answers
191 views
Can every sentence of first-order logic be converted into an equisatisfiable equation in Boolean algebra?
There may be some theoretical literature, unknown to me, that addresses this question. If possible, I would like a practical approach to this problem. My attempt involves the use of an equational ...
3
votes
2answers
85 views
How expensive is it to verify that a gate is universal?
I know that a NAND gate is considered universal because we can use it to implement an AND, OR, and NOT gate.
Given an arbitrary gate, or set of gates, how many operations would it take to verify if ...
0
votes
1answer
36 views
For a logic gate to be universal, must it necessarily be able to perform duplication?
It is said that a gate that can simulate AND and NOT is universal and able to recreate any classical circuit. I was looking at some of the circuits simulated by NAND, and for some of them, we need to ...
2
votes
1answer
25 views
first order logic to normal form order of operations
āyāx [A(x) ā§ B(y) -> C(x,y)]
āyāx [Ā¬(A(x) ā§ B(y)) v C(x,y)]
āyāx [Ā¬A(x) v Ā¬B(y) v C(x,y)]
I need to convert the above to conjunctive normal form. I'm a ...
-1
votes
1answer
55 views
1
vote
1answer
39 views
Universal Quantifiers in QBFs
I've been looking into reductions to/from the TQBF language and have managed to get stuck on something that is almost certainly not true (or, if it is true I'm missing a significant computational cost ...
0
votes
1answer
33 views
Lambda calculus simplification excercise
Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem.
(Ī»x.Ī»y.yx)z (Ī»w.w)
I am lost with this.
if anyone could lead me in ...
0
votes
0answers
23 views
Two variants of Fredkin gate
Sometimes two outpus of Fredkin gate are swapped when constant bit is 0, sometimes when it is 1. What variant is right or more modern? If it was conscious decision to change behavior what was ...
1
vote
0answers
20 views
In theory, should neuromorphic computers be more efficient than traditional computers when performing logic?
There is this general sentiment about neuromorphic computers that they are simply "more efficient" than von Neuman.
I've heard a lot of talk about neuromorphic computers in the context of ...
0
votes
1answer
23 views
Represent a DNF formula as a multivariate linear formula?
Lets say I have the following DNF: (x or y) and (z or i) / $(x\lor y)\land(z\lor i)$
How do I convert that into a polynomial form?
5
votes
1answer
36 views
Test two LTL expression trees for equivalence
Is there an algorithm on how to check if two LTL expressions (represented as binary trees) are semantically equivalent? Since there are many smaller equivalences such as
$a\Rightarrow b \equiv \neg a \...
0
votes
0answers
28 views
Building an ALU on nandgame's website
I'm working on nandgame's website found here. I'm working on the ALU and here is an image of my implementation:
My Implementation:
And I compared it to this website's solution:
Solution
However when ...
2
votes
0answers
39 views
Can HOL be simulated in the CiC?
I was wondering if HOL (higher-order logic) can be simulated in the Calculus of Inductive constructions (CiC)
2
votes
1answer
39 views
What were the shortcomings of Robinson's resolution procedure?
Paulson et alii. From LCF to Isabelle/HOL say:
Resolution for first-order logic, complete in principle but frequently disappointing in practice.
I think complete means they can proof any true ...
0
votes
0answers
47 views
Is a or free SAT formula NP complete?
Let $L$ be the languague which contains all satisfiable formulas which do not have the or symbol $\lor $.
Or more precise $$L=\{\phi | \phi \text{ is a satisfable formula which is only using the ...
1
vote
0answers
40 views
Is there a way to simplify redundant conditionals?
For example if I've this:
if a == false then return true else
if a == true and b == false return true else
if a == true and b == true then return false
can be ...
3
votes
1answer
134 views
How many clauses are required for SAT to be NP-hard in CNF formulas?
It is not hard to see that SAT for a CNF formula with $n$ variables and a constant number of clauses can be solved in polynomial time. On the other hand, it is not hard to see that a CNF formula with $...
0
votes
1answer
44 views
How are prime implicates of HORN-Formulas defined?
I'm confused about the definition of prime implicates in Horn formulas.
For example in the paper of Kira 2012 on page 109 it is stated:
Now in the paper of Boros 2010 on page 82 the following ...
0
votes
1answer
34 views
Equivalence of Horn formulas tractable?
Assume I have two Horn formulas $\phi_1, \phi_2$. Horn formulas are CNF formulas so that each clause has at most one unnegated literal. For example:
$x_1 \wedge (\neg x_1 \vee \neg x_2 \vee x_3 )\...
2
votes
2answers
72 views
Equivalence of Krom formulas tractable?
Assume I have two Krom formulas $\psi_1, \psi_2$. Krom formulas are propositional formulas in CNF that have 2 literals in every clause. Each literal can be negated or unnegated. In other words, $\...
0
votes
0answers
53 views
Note down the possible states in a truth table
You are required to automate the control of the water tank in your home. There are two water
contact sensors that turn to a TRUE state when in contact with water and a FALSE state when not.
Sensor $1 (...
4
votes
1answer
712 views
Question on the “Tutorial implementation of dependently typed lambda calculus”
I have a slight technical struggle with this marvelous tutorial. On page 5 the tutorial talks about typing rules for Simply Typed Lambdas and presents following judgement as derivable via rules on ...
0
votes
1answer
40 views
Consistent theory based on L and not(A->A) is a theorem
I am working on this problem in which I have a theory $T$ based on language $\mathcal{L}$ and the only information we have is that T is consistent and $\vdash \lnot(A \rightarrow A)$. Given this ...
1
vote
0answers
23 views
Impredicativity example in HOL
From these notes pages 37-38. In HOL, I'm giving the task of proving:
$\vdash \forall x^T. \forall y^T. (=_T x^T y^T) \implies (=_T y^T x^T)$
applying forall and implication introduction and the ...
0
votes
0answers
21 views
What is the best way to identify highly performing groups?
I am currently working on a project that involves sorting people into groups based on their ability to work well with others.
While it is a bit of a simplification, I have a problem that is ...
2
votes
1answer
15 views
Circuits and formulas for Clique
Is it correct to say that the Clique Problem is in $P$ iff there exists a family of Boolean circuits $C$ to decide Clique whose sizes are bounded by a polynomial? And based on this question, does that ...
1
vote
1answer
37 views
What is the theoretical result of flattening a list containing only itself?
Consider the following python code
X = [None]
X[0] = X
This has many fun properties such as
X[0] == X
and
...
3
votes
0answers
66 views
Understanding $\lambda \mu$-calculus in more programming way
I am learning $\lambda \mu$-calculus (self-study).
I learned it because it seems very useful for understanding Curry-Howard correspondence (e.g understanding the connection between classical logic ...
0
votes
0answers
28 views
Situation calculus: how to find pre-conditions in 15-puzzle game?
I have been working on finding the preconditions for a situation calculus example for some time now. This example is called the game "15-puzzle" where you can find a discription here https://...
0
votes
0answers
16 views
Can we use Axiomitization to decide CTL*?
As the title says. There are axioms for CTL*, but can we use them to decide whether a formula is satisfiable? We can use the trick $p$ is satisfiable $\iff$ $\lnot p$ is not valid. My problem is that ...
1
vote
1answer
52 views
Substitution lemma for types
TAPL (page 549) proposes the following lemma in order to prove soundness of System F type system:
Substitution lemma for types:
$E, X, \Delta \vdash t: T \implies E, [X \mapsto S] \Delta \vdash [X \...
0
votes
0answers
29 views
Show that exist a finite set of clauses F in first-order logic that Res*(F) is infinite
I'm kind of desperate at this point about this question.
A predicate-logic resolution derivation of a clause $C$ from a set of clauses $F$ is a
sequence of clauses $C_1,\dots,C_m$, with $C_m = C$ ...
2
votes
1answer
37 views
Unification Algorithm without Occur Check
I have been reading about Unification algorithm here https://en.wikipedia.org/wiki/Unification_(computer_science)#A_unification_algorithm
. And I wonder about the importance of occur check.
I know ...
1
vote
1answer
32 views
Proving a certain primitive recursive function exists
Assume $f\colon Ļ Ć Ļ ā Ļ$ is a computable function. How can we prove that there is a primitive recursive function $g\colon Ļ Ć Ļ ā Ļ$ where the following holds:
$ān [ās(f(n, s) = 1) ā āk(g(n, k) = 1)...
0
votes
1answer
35 views
Z-Specification = Routes
Im trying to make an invariant for this Z schema about routes.
1) The invariant should express that each route should contain at least 20 different places. First of all i thought of doing a universal ...
