Stack Exchange Network

Stack Exchange network consists of 174 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

1
vote
0answers
91 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
238 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
90 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
227 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
16 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
423 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
37 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
780 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
92 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
27 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
169 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
822 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
97 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
16 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
51 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
191 views

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

I have following unfinished proof of a lemma: ...
2
votes
2answers
54 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
274 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
43 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
321 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
112 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
69 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
325 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. ...
0
votes
1answer
40 views

Does every 3CNF propositional formula has an equisatisfiable 2CNF propositional formula

Does every 3CNF propositional formula has an equisatisfiable 2CNF propositional formula?
1
vote
1answer
72 views

Does every 3CNF propositional formula has an equivalent 2CNF propositional formula?

Does every 3CNF propositional formula has an equivalent 2CNF propositional formula? Definitions: 3CNF propositional formula is conjunctive normal form propositional formula, which is just ...
1
vote
1answer
102 views

Boolean Logic Equation

How can I prove this. what is the way? im up to the second last line. and i dont actually know how can x * (1 + y) then the y just disappears into x * 1. ...
0
votes
0answers
28 views

Resolution with multiple variables

Resolution allows to generate new clauses for an existing set of clauses. In many cases, the rule is simple: ...
3
votes
1answer
149 views

How would one use “BUT” logic in a ternary logic computer in a practical way?

Using three valued logic one can define a multitude of ternary operations. When dealing with 5:3:1[1] operations, its very easy to see how ...
5
votes
1answer
107 views

Procedure to automatically solve field theorems in a SMT solver

I'm working with the Welder proof assistant. Basically, this system uses basic inference rules to modify the goal one wants to proof. At a latter step, the modified goals are passed to a SMT solver to ...
0
votes
0answers
63 views

Convert conjunctive normal form to equivalent boolean formula with only NOR gates

Let $\varphi$ be a boolean formula in 3-CNF form (conjunctive normal form with three literals at most per clause). I want to convert it to an equivalent boolean formula that uses only NOR gates with ...
1
vote
1answer
180 views

Generalization of Horn clauses in logic programming?

As far as I understand, Prolog and related languages are restricted to inference rules of the form $$ p_1 \land \dots \land p_n \rightarrow q$$ which is equivalent to the Horn clause $$ \neg p_1 \lor \...
0
votes
1answer
199 views

Convert conjunctive normal form to equivalent boolean formula with only NAND gates

Let $\varphi$ be a boolean formula in 3-CNF form (conjunctive normal form with three literals at most per clause). I want to convert it to an equivalent boolean formula that uses only NAND gates with ...
0
votes
1answer
55 views

Someone explain the Venn diagram for the logic equation (A+B)(B+C)

I posted a similar question here, however I have another question regarding Venn diagrams and logic circuits... In this problem: $$(A+B)(B+C)$$ Wouldn't the Venn diagram look something like this? ...
2
votes
2answers
159 views

Someone explain the venn diagram for the logic equation A*(B+C)

So, I am studying logic circuits and how to prove them with Venn diagrams. When drawing a Venn diagram for the equation A*(B+C) I figured it would look something like this: But according to the ...
1
vote
1answer
281 views

Is this possible to solve boolean satisfiablility by using karnaugh maps to simplify the whole given boolean formula by simplifying subformulas?

Building karnaugh map for the whole given boolean formula always costs Θ(2n) both time and space complexities, where $n$ is the number of boolean variables in the given boolean formula. It is ...
4
votes
1answer
214 views

How do you represent LISP as mathematical / logical model?

I asked this in stackoverflow, but the question probably fits here better. This question arose from the objection that LISP is regarded as a functional language with some simple principles, namely ...
1
vote
1answer
30 views

What is the largest possible minimal 3CNF formula as function of the number of variables?

I have already defined here what is minimal 3CNF formula. In the answer to the question, D.W. answered: What you are thinking is wrong. A minimal, unsatisfiable formula can have more than 8 clauses. ...
3
votes
0answers
39 views

Sorts and constructors for modelling classes in a theorem prover

I have been working in the Welder theorem prover for some time now. But I'm confused in the way they handle data-types. I'm not familiar with the terminology of sorts and constructors. Here is how one ...
2
votes
1answer
59 views

What is the set of all maximal 3CNF formulas?

Definition: A maximal 3CNF formula is satisfiable 3CNF formula, but if you conjuct it with another any new different 3 disjuctive literals clause, then the formula becomes unsatisfiable. Please don't ...
1
vote
0answers
25 views

Satisfaction Complete Theories

From Counterexample-Guided Quantifier Instantiation for Synthesis in SMT: a $\Sigma$-theory $T$ is satisfaction complete with respect to $L$ if every $T$-satisfiable formula of $L$ is $T$-valid.......
1
vote
1answer
147 views

What is the complexity of determining whether or not conjunction of positive CNF and negative CNF is satisfiable?

Definitions: positive CNF is a conjunctive normal form formula, where all literals are positive, i.e. the unary connective ¬ does not exist in the formula. negative CNF is a conjunctive normal ...
10
votes
1answer
191 views

Is there a dual concept to “Turing Complete” in logic?

Two computing models can be shown to be co complete if each can encode a universal simulator for the other. Two logics can be shown to be co complete if an encoding of the rules of inferences (and ...
2
votes
3answers
77 views

Linear Temporal Logic with non-Boolean propositions (e.g. Integers)?

LTL works with Boolean propositions. People probably studied extensions to non-Boolean propositions... Do you know a good starting reference? (I am aware of STL, but it also seems to talk about ...
2
votes
1answer
96 views

What is the set of all minimal 3CNF formulas?

Definition: A minimal 3CNF formula is an unsatisfiable 3CNF formula with minimum clauses connected by conjunctions, where each clause is disjunction of 3 literals, that is if any of it's clauses is ...
1
vote
1answer
72 views

What should I read before tackling Michael Huth's Logic in Computer Science: Modelling and Reasoning about Systems?

I have to read Logic in Computer Science: Modelling and Reasoning about Systems by M. Huth and M. Ryan for a class next semester. However Amazon reviews say it's hard to read unless you're an advanced ...
1
vote
1answer
43 views

Logic, “and” operator between a set of formulas and a formula

Consider a set $S$ of formulas $\beta_i$ and a formula $\alpha$, if we have a condition such as $S \land \alpha$ is inconsistent what we have to calculate to check the inconsistency of $S \land \alpha$...
3
votes
1answer
228 views

Semantic readings of the Lambek sequent calculus

I am reading Categorial Grammar: Logical Syntax, Semantics, and Processing by Glyn Morrill and I am stuck with the Fig. 3.9: Can someone explain this set of formulas and |.| function specifically? ...