Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [logic]

Questions related to mathematical logic and its use in computer science

0
votes
0answers
36 views

Finding the value of y for given equation?

Given the equation : x & y = x, where x, y are positive integers. Note: Here '&' stands for Bitwise operator AND between two numbers. I am provided with the value of x. Can I find possible ...
3
votes
3answers
202 views

Does exist any horn formula that is equisatisfiable to the clause that is disjunction of two literals? Does also exist equivalent?

I just and simply want to know if whether or not exist any horn formula that is equisatisfiable to $(p\lor q)$. I would also be interested to know if there also exists equivalent.
2
votes
1answer
67 views

Why doesn't this put $BPP$ in $NP$?

From Sipser Gacs we know $x\in L(M)$ for a machine $M\in BPP$ $\iff$ $$\exists t_1,\dots,t_{|r|}\forall r\in\{0,1\}^{|r|}\vee_{i\in\{1,\dots,|r|\}}M(x,r\oplus t_i)=1.$$ From Adleman we know $x\in L(M)...
3
votes
1answer
66 views

Validity of this formula in WS1S logic

The following formulas are said to be defined in WS1S logic. $Closed(Z, R) := ∀x ∀y(x ∈ Z ∧ R(x, y) → y ∈ Z)$ $(z_1, z_2) ∈ R^∗ := ∀Z.(z_1 ∈ Z ∧ Closed(Z, R) → z_2 ∈ Z)$ However since WS1S formula ...
1
vote
1answer
164 views

Explanation of the Gelfond Lifschitz reduct

Can someone explain with a hands on example how the Gelfond Lifschitz reduct works in order to check stable model semantics? edit a simple example here - at least as far as I understand the thing. ...
1
vote
0answers
23 views

how to use the solution of mean payoff game to arrive at winning regions of parity game?

The 7th chapter (7.3 section) of "Automata Logics and Infinite Games" by Erich Gradel, Wolfgang Thomas, Thomas Wilke gives a way to convert max parity game to mean payoff game. I do not understand ...
3
votes
1answer
78 views

Programmatically checking equivalence of statements

So as part of a theorem-prover/checker, I'm using Prolog to try to determine the equivalence of statements that have been parsed into tree form, e.g. $x=2$ is represented as ...
2
votes
0answers
50 views

Automatic learning/discovery of logics

Are there efforts to automatically discover new logics? Logics are simple structures - they have formal language, deduction rules, semantics and certain properties that are proved or discarded for ...
3
votes
0answers
83 views

Semantic parsing with Grammatical Framework - is this possible?

So far I have learned about categorial grammars, type logical grammars and formal semantics of natural language, the relevant tools are Cornell Semantic Parsing Framework https://github.com/clic-lab/...
-1
votes
1answer
280 views

Must algorithm for comparing numbers investigate all bits?

Suppose algorithm $A$ on a digital computer takes as input integers $x$ and $y$ in binary. The algorithm outputs one if $x=y$, and zero if $x \neq y$. Is there a proof that for any input $x$ and $y$ ...
1
vote
1answer
81 views

Proving that a Turing machine decides a language in NP

Suppose a deterministic Turing machine T decides language L and L is in NP. Then must it be provable in ZF that T decides L?
0
votes
1answer
301 views

Logic Circuits - Binary divisible by 16 [closed]

I have a question ...
2
votes
2answers
298 views

Max() in Domain Relational Calculus

I was looking through my notes on domain relational calculus, and noticed an interesting result in a question about finding the most expensive pizza(s), given a pizza table with schema $\text{pizza}(\...
0
votes
1answer
59 views

Given two formulae E[G F p] (which is CTL*) and EG EF p ( which is a CTL) with a Model prove that they are not equivalent

I am trying to prove they are not equivalent , a model which satisfies the fist one but not the second since I think EG EF p is stronger than E[GF p],any leads would be helpful. Thanks.
0
votes
2answers
335 views

Two's complement 8-bit subtractor? [closed]

Please help me! I've been asked to make a circuit using only Logic Gates to implement an 8-bit 2's complement subtractor. I was thinking of somehow modifying an 8-bit adder, but I figured it isn't 2'...
3
votes
0answers
67 views

Passing arrays vs functions as arguments in SMT?

In SAT Modulo Theories (SMT), with the theory of uninterpreted functions, all functions are first order, that is, they don't take functions as arguments or return functions. In the theory of arrays, ...
1
vote
1answer
84 views

Complexity of 1-in-3 SAT variant with restrictions on “unique” variables per clause

I'm interested in the complexity of a particular variant of 1-in-3 SAT. Assume, as is usual, that clauses are allowed to be of length 1, 2, or 3. Then add the restriction that for any clause of length ...
0
votes
2answers
115 views

How to convert 2 or gates (x1 V x2 V x3) to NAND

How can I convert a clause of size 3 that is made of 2 OR gates example: (x1 OR x2 OR x3 ) to one or more clauses of size 4 made only of NAND ...
1
vote
3answers
114 views

How does maths consistency impacts on computer science?

Lot of mathematicians have made several efforts to answer the question : are mathematics consistent ? Although we haven't yet had a proof of consistency, and surely we will never (Gödel second theorem)...
2
votes
1answer
234 views

Draw a function by only using two input NOR gates [closed]

T = (BD + A'BC'+A'CD) How can i draw this by only using NOR-Gates? This is what i have done so far: https://imgur.com/a/JG2eU Have I understood this right?
1
vote
0answers
55 views

Hoare correctness proof for a recursive definition of multiplication

Given the program: {y=y0 ^ y>=0} z=0; while (y>0){ z=z+x; (1) y=y-1; } {z=x*y0} I am having trouble finding the ...
5
votes
2answers
164 views

Undecidable predicate logic is decidable by people?

Logic in computer science (By Michael Huth,Mark Ryan, second edition, page 132) says Every φ can, in principle, be discovered to be valid or not, if you are prepared to work arbitrarily hard at ...
4
votes
0answers
37 views

Modern presentation of Ackermann's “Solvable Cases?”

Ackermann's book "Solvable Cases of the Decision Problem" discusses decidable instances of first order logic, particularly monadic logic, and so called "equality formulas". However, the book is from ...
1
vote
1answer
62 views

What is the transitive and reflective closure of the derivation relationship?

This question is asked during a class of Computer Science. What is the transitive and reflective closure of the derivation relationship? I know that if $R$ is a relationship on $A^2$, a ...
1
vote
0answers
96 views

DPLL algorithm for 3SAT [closed]

This question is from my complexity theory course. How to change the standard DPLL algorithm for SAT in order to solve 3-SAT instances? The general DPLL algorithm for SAT is defined: ...
11
votes
1answer
300 views

Monadic Second Order Logic for Dummies

I am programmer with a grip on automata, but not on logic. I read in papers that the two are very tightly related. Deterministic Finite Automata (DFA), Tree Automata and Visibly Pushdown Automata are ...
4
votes
1answer
99 views

How logic programming (especially ASP) is related to the reasoning in (first-order) logic?

How logic programming (https://en.wikipedia.org/wiki/Logic_programming, especially answer set programming) is related to the reasoning in the (first-order) logic? Maybe logic programming can be ...
-1
votes
2answers
262 views

Can we apply De Morgan's to any operator? (boolean , arithmetic , relational)

I have seen various statements with negation( or complement) operators and when i try to negate them using De Morgan's law , i become confused about how to negate. The main doubts are what variables ...
0
votes
1answer
21 views

Defining a predicate on the structure of a string

I have the following homework question. (For a bit of context - the study unit is Formal Languages and Automata). Define the predicate $\mathrm{pre}(s,t)$ over $s, t\in\Sigma^*$ by induction on the ...
1
vote
0answers
18 views

Subsymbolic/multimedia knowledge - query, creation and reasoning? Reference request?

One can consider multimedia data as a matrix of pixels, but, of course - multimedia data contains higher-order knowledge as well. E.g. everyone can describe famous paintings in terms of colours, ...
0
votes
1answer
511 views

Greater than or equal to operation (32-bit ALU)

I'm trying to construct a greater than or equal to operation by adding some logic gates or building blocks (i.e. multiplexor and decoder) to my current 32-bit ALU I'm not quite sure how to do this ...
1
vote
0answers
43 views

Unable to have an equivalent of A(FG p) and AG(EF p)

It states in my lecture notes that there is no CTL formula that is equivalent to A(FG p) in LTL and likewise, there is no LTL formula that is equivalent to CTL formula AG(EF p). I am just starting to ...
21
votes
11answers
4k views

Why is $A \lor (A \land \neg B) \equiv A$?

I would like to know if there is a rule to prove this. For example, if I use the distributive law I will get only $(A \lor A) \land (A \lor \neg B)$.
1
vote
1answer
1k views

Show that a language consisting of strings of a prime number of 1s is irregular using pumping lemma [duplicate]

Question: L is a language defined as $\ L = \{1^l | l\in primes\}$ (strings of 1s having a prime length). Show that this is not a regular language ($\ L \notin REG$). You may either use the theory ...
-4
votes
1answer
100 views

Valid, unsatisfied or neither? [closed]

How should I create the truth table to solve each of these questions? Maybe can give me an example? $Smoke \implies Smoke$ $Smoke \implies Fire$ $(Smoke \implies Fire) \implies (\neg Smoke \implies \...
4
votes
0answers
30 views

Quantum algorithms for logical inference - reference request?

Microsoft is committed to the building of the scalable, industrial size topological quantum computer, Visual Studio integrated programming language and SDK will be released by the end of this year (...
2
votes
4answers
181 views

Is it necessary to learn how to prove Mathematical theorems as a CS Student? [closed]

I've just started my undergraduate course and have tried my hands on MIT's OpenCourseWare on Discrete Math on Logic and Proofs. There was a particular question asking to prove Cantor's Theorem: ...
5
votes
2answers
823 views

Do we have knowledge bases only because the logics are not automated enough?

Do we have knowledge bases only because the logics are not automated enough? I.e. - is it true, that the ideal situation would be that we use the set of logical formulas as the knowledge base together ...
1
vote
1answer
107 views

positivity condition in Coq/CIC

I am recently learning the theory behind Coq and learnt that positivity condition guarantees termination of the program. But my question is, what would you think of the following definition? ...
0
votes
0answers
17 views

sorting data to provide top entries

I have a table like below. Each row has store id, discount % for one of their coupons. Each store could have multiple coupons but (store+discount %) is a primary key. I would like to find out top 10 ...
1
vote
0answers
57 views

Universal theorem proving algorithms for sequent calculus (e.g. for cut-free logics)?

Some of the logics admit Gentzen-style sequent calculus. Are there universal algorithms that allow to find proof (derivation of the proof) in sequent caculus for every hypthetical theorem? Some of ...
5
votes
1answer
210 views

What does instantiating existential variables with out of scope variable imply?

I have following unfinished proof of a lemma: ...
2
votes
2answers
55 views

Any Non-trivial Logic System Defined with only Equality

Preface We can define a system of logic by conjunctions of rules that system must follow. For example, if we wanted to define transitivity of numbers: $$F_1: \forall a,b,c. a < b \land b < c \...
3
votes
1answer
275 views

How come identity encodes absurdity

From P5 in this paper: https://hal.inria.fr/hal-01094195/file/CIC.pdf Using this purely functional part, it is possible to encode many int eresting notions. For instance ∀ C : Prop , C ...
2
votes
1answer
44 views

Simple discrete math problem: A and B in 3CNF

I need to write (A and B) in 3CNF, and for whatever reason, I can only come up with (A or B) in 3CNF (A OR B OR X) AND (NOT(X) OR A OR B). Any help is greatly appreciated!
1
vote
0answers
47 views

How to find states in logic circuits?

For hobbyist reasons I wrote a program which takes the equations of the logic gates of a digital circuit as input, does some analysis, outputs the analysis results and generates program code for doing ...
1
vote
2answers
407 views

Algorithm for determining if a statement is a paradox

Please bear with me, since I have just started working on this. Assuming that the laws of thought apply. The basic goal of the algorithm is to recast the statement into true or false premises and ...
0
votes
1answer
145 views

cancel out parts of a formula in CNF (conjunctive normal form)

In this image there is a given formula in DNF and CNF. When I check it on Wolfram Alpha I see that it cancel out (E or D) because of (not A or A) which is colored in red. My question is if it is ...
1
vote
1answer
71 views

Is it an open problem if generalized resolution is always possible?

Let we have a 3CNF under following restriction: each variable occurs 3 times. Then I apply generalized resolution (GR) (I don't know which name would fit more) technique (number of clauses can be ...
4
votes
1answer
374 views

What is random logic? Why is it needed?

I read now several articles about RISC and CISC architecture. Most are rather exuberant enumerating all the differences between these architecture, but not necessarily why things are the way they are. ...