Questions related to logic and its use in computer science
0
votes
0answers
15 views
Start using SAT Solvers
What i actually want to do is to turn a math problem ,i have to solve,to a Boolean Satisfiability problem and solve it using a SAT Solver.
I wonder if someone knows any manual,guide or anything that ...
0
votes
0answers
45 views
f(n) output of universal program
I have a question concerning an universal program (goto program). Well, let $f(n)$ be the output of an universal goto program $U$ with input $(n,n)$, where the first $n$ describes the encoding and the ...
0
votes
0answers
18 views
Description Logics within a context
Trying to get grips with DL and OWL. The context is TV Programmes. I wrote in words the first sentence which I want to convert into DL:
Each broadcast hasOneOrMore Episodes
Each episode ...
1
vote
1answer
40 views
Proof of Trakhtenbrot's theorem
In the proof of Trakhtenbrot's theorem (as given in "Elements of Finite Model Theory" by Leonid Libkin), for every Turing machine $M$, author constructs a FO sentence $\Phi_M$ of vocabulary $\sigma$ ...
3
votes
2answers
38 views
Temporal logic for interface invariants
I am looking for some sort of temporal logic for expressing invariants in interfaces. Since interfaces do not specify data representation, the invariants must rely solely on the publicly available ...
2
votes
2answers
59 views
TQBF as interactive game
My teacher describes true quantified boolean formula (TQBF) as an interactive game between two players $\exists$ and $\forall$, and asks us to show a winning strategy for the existential player ...
4
votes
1answer
43 views
What is the exact difference between a latch & a flipflop?
From what I have understood :
A Flip Flop is a clocked latch i.e. flip flop = latch + clock
Latch continuously checks for inputs & changes the output whenever there is a change in input
Flip ...
1
vote
2answers
61 views
Understanding DPLL algorithm
I'm trying to understand DPLL algorithm for solving SAT problem. And here it is:
...
1
vote
1answer
82 views
Why S=1, R=1 Is forbidden in RS-Flip Flop [closed]
I have come across about RS Flip Flop & I have tried implementing that on a simulator & using actual logic gates. But I'm still not sure whether I have correctly understood the case unstable ...
4
votes
0answers
98 views
Decidability over finite graphs of small degree
Suppose $\sigma$ is a vocabulary of First Order logic consisting of one binary relation $E$ and let $\phi$ be a $\sigma$ sentence (FO formula with no free variables). Is it decidable whether there is ...
1
vote
3answers
66 views
Loop Invariants as Tautologies
Would it be correct to characterize loop invariants as a type of tautology? I ask since the invariant must basically always be true, before the loop starts, before each iteration and after the loop ...
1
vote
1answer
32 views
Expressing complexity class P using first-order logic with LFP
Can anyone show how to express complexity class P using first-order logic with LFP? (descriptive complexity)
1
vote
2answers
49 views
Proving non-confluency and adding an equation to make it confluent and terminating
I currently have a system that has {f(a) = b, f(f(x)) = x} (part of an exam question - look at page 5 - exercise 1).
To start off with proving non-confluency, I am ...
0
votes
3answers
117 views
Can P=PSPACE and PSPACE problems be formulated as $\Pi_1$ formula?
To say simply, can PSPACE problems be written as $\Pi_1$ formula? Or how can these problems be written in terms of (first-order) arithmetic hierarchy?
edit:also currently, by what arithmetic ...
3
votes
2answers
77 views
Formulas vs Circuits
In boolean circuit complexity, a circuit is just defined by a Directed Acyclic Graphs with designated input and output nodes, where the intermediate nodes compute a specific boolean function. A ...
6
votes
3answers
135 views
anonymous lambda functions (functional programming)
What are anonymous (lambda) functions? What is the formal definition of an anonymous function in a functional programming language?
In my simple terms, when I am programming in scheme/lisp I would ...
3
votes
2answers
30 views
Creating a logical circuit
Task:
Design a 2 bit comparator.
Input: 2x 2 bit (I take it as 2 2-bit values, let them be unsigned for simplicity)
Output: 1 if result input1>input2 is true, 0 otherwise
Develop truth table and ...
5
votes
2answers
106 views
Clear, intuitive derivation of the fixed-point combinator (Y combinator)?
The fixed-point combinator FIX (aka the Y combinator) in the (untyped) lambda calculus ($\lambda$) is defined as:
FIX $\triangleq \lambda f.(\lambda x. f~(\lambda y. x~x~y))~(\lambda x. f~(\lambda y. ...
1
vote
1answer
52 views
Difference between intended interpretation and extended interpretation in first-order logic
I am currently reading "Artificial Intelligence - A modern approach" and I really do not get the difference between intended interpretation and extended interpretation in first-order logic.
Are ...
0
votes
0answers
51 views
Converting first-order formula to CNF
I need to convert this statement to CNF (Conjunctive normal form):
$\qquad \left((\forall x.\, P(x)) \implies Q(a)\right)\implies \left((\exists y.\, P(y)) \implies Q(a)\right)$
I got this answer:
...
2
votes
1answer
44 views
Description of resolution algorithm as it applies to SAT
SAT [5] can be solved with resolution definitively, i.e. if the formula has a true assignment, resolution can find it, and if it cant be satisfied, resolution can show that no assignment exists (at ...
2
votes
1answer
68 views
Building functionally complete boolean circuits out of trinary logic
There are some not-very-commonly considered forms of trinary logic using 3 truth values. Even entire (unusual/rare) ternary computers have been built from it.
Is there some knowledge or reference ...
2
votes
1answer
45 views
MGU and Variable Standardization - CNF
I have been reading on converting first order logic sentences to conjunctive normal form, and then performing resolution.
One of the steps of converting to CNF, is to Standardize variables: rename ...
1
vote
2answers
77 views
Is resolution complete or only refutation-complete?
Going through some knowledge representation tutorials on resolution at the moment, and I came across slide 05.KR, no77.
There it is mentioned that "the procedure is also complete".
I think this ...
2
votes
1answer
44 views
Convert CTL* formula to CTL
I have a CTL* formula: $\mathsf{EF}[p\land \mathsf{AX}[q\ \mathsf{U}\ r]]$ but in my application, I am limited to CTL. To my understanding, this formula is no valid CTL and I wonder whether I can ...
2
votes
2answers
166 views
The difference between a sequence and a set
I am new to discrete mathematics and the theory of computation I am trying to learn and understand the terminology.
I am having a difficult time understanding the difference between a set and a ...
3
votes
2answers
154 views
“Applicative order” and “Normal order” in lambda-calculus
Applicative order: Always fully evaluate the arguments of a function
before evaluating the function itself , like -
$(\lambda x. x^2(\lambda x.(x+1) \ \ 2))) \rightarrow (\lambda x.
...
3
votes
1answer
87 views
Propositional formula in DNF can be decided in polynomial time?
For a given propositional formula f in DNF, one can decide in polynomial time, if the formula is satisfiable:
Just walk through all subformulas (l_1 and ... and l_k) and check, wheter it has NO ...
2
votes
1answer
67 views
LTL: Show $\neg(aUb) \Leftrightarrow \neg b U (\neg a \land \neg b) \lor G \neg b$
I got as far as
\begin{align}
w \vDash \neg (a U b) &\Leftrightarrow \neg (w \vDash a U b)
\Leftrightarrow \neg (\exists_{i\geq0} : w^i \vDash b \land \forall_{0\leq k < i} : w^k \vDash a) ...
2
votes
1answer
64 views
How is verifying whether an assignment satisfies a boolean formula possible in polynomial time?
How can I prove that I can verify whether a boolean assignment of variables $a$ satisfies some boolean formmula $\phi$ in polynomial time?
I know that we can just plug the boolean assignment into the ...
5
votes
1answer
93 views
Question related to Hilbert's 10th problem
Given $n \in \mathbb{N}$ and $p,q \in \mathbb{N}[x_1,\ldots,x_n]$ one can define the following formula in the language of formal arithmetics
$$\varphi(n,p,q) = \forall x_1 \cdots \forall x_n : \neg ...
3
votes
0answers
191 views
Has someone seen this structure before?
I am working 1 with a certain structure,
and I wonder if someone has seen it before.
I am no mathematician, so all I can say is that
I will do my best to describe this structure.
It is actually very ...
3
votes
1answer
115 views
A programming language that can only implement computable bijective functions?
Are there programming languages(or logic) that can implement(or express) a function $f:\mathbb{N}\to \mathbb{N}$ if and only if $f$ is a computable bijective functions?
1
vote
1answer
62 views
What courses to learn for artificial neural networks and machine learning? [closed]
http://www.scotthyoung.com/blog/mit-challenge/#1
This guy's work is mind blowing. He learned the 4 year MIT CS curriculum in 1 year, at home through opencourseware. I want to get into artificial ...
3
votes
1answer
50 views
Are two terms where one is without a $\lambda\beta$ normal form unconvertible in $\lambda\beta$?
I know that if you try and make the theory
$$\lambda\beta+\{s = t\ |\text{ s, t are terms without }\lambda\beta\text{ normal forms}\}$$
then that theory becomes inconsistent. Are two terms where one ...
3
votes
1answer
48 views
Equivalence of GFp and Gp in LTL
In linear time logic, is $\mathbf{GF}p$ equivalent to $ \mathbf{G}p$ ?
$\mathbf{GF}p$ means that it is always the case that p is true eventually.
Let $\mathbf{G} p$ be defined as: $\forall j \ge0,\ ...
3
votes
2answers
119 views
First-order logic arity defines decidability?
I've read first-order logic is in general undecidable, and that could be decidable only when working with unary operators. (I think that's propositional logic, correct me if I am wrong)
The question ...
0
votes
1answer
55 views
Resolution and incomplete Knowledge Base
Assume I have an incomplete knowledge base, for example:
...
0
votes
0answers
47 views
How would this hierarchy for knowledge representation be extended?
I've tried making a hierarchy of all forms of knowledge - including physical objects, numbers, procedures etc. How could this be improved? How would a sentence such as "Jack is producing music sitting ...
3
votes
0answers
46 views
Spot the formalism (some kind of process logic)
Consider the following specification technique.
A specification consists of a finite set of triples $\langle C, A, C' \rangle$,
where $A$ is the name of an action and $C, C'$ are conditions, that is,
...
0
votes
1answer
36 views
Given the phrase “Where NONE of the following are TRUE” and two statements how should a boolean logic be composed?
Let's have two statements
(value > 10)
(value < 25)
And a list of items with the following values
10
20
30
This is what a truth table would give
...
3
votes
1answer
67 views
Universality of NOT and CNOT
I'm trying to figure out why NOT and CNOT gates are not sufficient to create all bijective functions in classical circuits. I have been struggling on this for hours, and just can't make sense of it.
...
3
votes
2answers
226 views
Lambda Calculus simplification
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.
$$(\lambda mn.(\lambda sz.ms(nsz)))(\lambda sz.sz)(\lambda ...
2
votes
1answer
58 views
How to make a parse tree for the following propositional logic formula?
I have a formula $ \neg((q \implies \neg q) \vee p \vee (\neg q \implies (r \wedge p))) $.
As it contains 3 subformulas between the $\vee$'s, how can i put it into a parse tree, as a parse tree ...
4
votes
1answer
85 views
How many possible assignments does a CNF sentence have?
I'm having some trouble understanding the following:
When we look at satisfiability problems in conjunctive normal form, an underconstrained problem is one with relatively few clauses constraining ...
2
votes
1answer
66 views
definition of formula validity
I read in some sources that valid formulas are tautologies (valid under every evaluation). In the others, I read that these are formulas that have conclusions true when premises are true. Are these ...
7
votes
1answer
108 views
Redundancy elimination in the superposition calculus
When proving theorems with the superposition calculus, we deal with three kinds of rules:
Generating rules: from pair of clauses A and B, generate new clause C while keeping the original pair, e.g. ...
2
votes
1answer
112 views
Negation of nested quantifiers
The problem is:
$$\exists x \forall y (x \ge y)$$
With a domain of all real positive integers.
The negation is:
$$\forall x \exists y (x < y)$$
so, if $y = x + 1$, the negation is true.
That ...
0
votes
2answers
131 views
Predicate Logic Paradox [duplicate]
Possible Duplicate:
Negation of nested quantifiers
The problem is:
∃x∀y(x ≥ y)
With a domain of all real positive integers.
The negation is:
∀x∃y(x < y)
so, if y = x + 1
the ...
4
votes
2answers
147 views
The meaning of modulo in “formula modulo a background theory”
I have been reading some papers where I keep reading stuff like “first-order formula modulo a background theory”. Does anyone know what modulo means in this case ? Is it something like “with respect ...
