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
1answer
42 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
97 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
115 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
30 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
154 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
129 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
71 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
211 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
251 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
64 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
163 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
325 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
240 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
32 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
40 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
67 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
164 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
195 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 ...
3
votes
3answers
92 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
100 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
74 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
232 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? ...
2
votes
0answers
167 views

Recursive definitions, How it is done?

I read that recursive definitions, refer to the definition of a function in that function body, cannot be done in $\lambda$-calculus, but recursion can be achieved by using $Y$ combinator. As I know, ...
2
votes
0answers
77 views

Unification algorithm - need clarification

I have these two terms: {P(a,x,x),P(a,b,c)} I'm supposed to find if the terms and unifiable using the unification algorithm. I'd do the following substitutions: b/x, resulting in : {P(a,b,b),P(a,b,...
0
votes
1answer
135 views

Why does (y < 10) imply everywhere (x > 0 ^ y < 10)?

My lecturer recently released solutions to an assignment. One of the questions was to determine the weakest precondition of: ...
5
votes
0answers
126 views

Characterization of alpha-equivalence in languages with bindings

Following up on this post denoting $(x \leftrightarrow y)$ the permutation of $x$ and $y$ and $P[x \leftrightarrow y]$ the term obtained from the term $P$ by permuting $x$ and $y$ (so for example if $...
7
votes
1answer
476 views

Algorithm for deciding alpha-equivalence of terms in languages with bindings

I am interested in the alpha equivalence relation in languages with variable bindings, such as: ...
2
votes
0answers
75 views

How to know whether a formula is common knowledge in Kripke structure?

Suppose that we have a formula A which is valid in all states of Kripke structure and some transition relations. Is it generally possible to derive if formula A is common knowledge between particular ...
2
votes
1answer
116 views

First Order Logic : Predicates

I have a small problem with the first order logic, in particular, predicate logic Let us take this sentence as an example: ...
3
votes
1answer
777 views

Turing-completeness, Conway's Game of Life and Logical Gates

I was recently given an assignment at university asking me to discuss the universal computational capability of Conway's Game of Life. I'm not required to actually build up a Universal Turing machine ...
-3
votes
1answer
76 views

How to negate this one?

How can I negate the following sentence: For all words x from L with |x|>= n , exists decomposition x = uvw with |uv| <= n and |v| >= 1, so for all i >= 0 , is valid that u(v)^iw in L is.
1
vote
0answers
89 views

Computing critical pairs, confluence and Normal terms

Down below is a Term rewriting system where I am trying to find the critical pairs, decide if it is confluent and find the Normal terms. I think it's difficult to understand all these concepts and I ...
1
vote
0answers
219 views

Propositional logic in an SMA* algorithm

I'm trying to implement an SMA* graph search algorithm that I found in a paper here(Rong Zhou, Eric A. Hansen: Memory-Bounded A* Graph Search. FLAIRS-02 Proceedings 203-209) and I would like to ...
1
vote
2answers
301 views

Induction rules for reflexive, transitive closure

I'm trying to solve an exercise on inductive definitions, the premiss is: Let $\to$ be a relation on $A$ and $\to^*$ its reflexive, transitive closure, which is defined by following two rules: $a \...
1
vote
1answer
68 views

Secretary Problem with 2 positions - Maximizing the difference

Synopsis Imagine the secretary problem, except the goal is to hire two secretaries with the greatest possible difference between the two. The Problem I'm not particularly comfortable with this ...
2
votes
1answer
85 views

Are these examples of unification problems?

I have been studying unification, especially nominal unification (paper) gets my attention. I read the theory and examples. But I am wondering that what kind of problems occur in unifications. For ...
1
vote
1answer
481 views

Why does radix sort work?

I understand how radix sort works and how to implement it, but I don't understand why it works. Are there any underlying mathematical or logical principles that it relies on?
1
vote
1answer
41 views

Building a verifier for sentences involving addition over the natural numbers

Consider the model $(\mathbb{N},+)$; that is, the natural numbers equipped with the addition relation, PLUS($x$,$y$,$z$), where PLUS($x$,$y$,$z$) is true iff $x + y = z$. Let Th$(\mathbb{N},+)$ be the ...
1
vote
0answers
127 views

Understanding quantifiers

I'm reading a paper by David Monniaux An encoding of array verification problems into array-free Horn clauses. Second page Line 10: "Very often, desirable properties over arrays are universally ...
2
votes
0answers
95 views

Satisfying of $\square (\neg A \cup B)$

Let's consider the following formula: $\square (\neg A \cup B)$. Does the following computation satisfy it? The numbers in brackets are number of state. (0) $\neg A, \neg B$ (1) $\neg A, B$ (2) $...
2
votes
1answer
85 views

Showing $1$-reducibility of $\overline{\text{HALT}'}$ to index set

Note: overline denotes complement I am trying to show that $\overline{\text{HALT}'}\leq_1 \{i\colon\Phi_i=\Phi_e\}:= A$ for some fixed $e$ but I am misunderstanding the problem or method and can't ...
1
vote
1answer
78 views

What kind of LTL formula can be represented by DBAs

I am looking for the portion of LTL formula that can be expressed by deterministic buchi automata. Is there any classification of this such?
3
votes
1answer
197 views

Expressing a logical constraint in integer programming

Let $x$ be an integer such that $x \in [ - 10,10]$ and $b$ a binary variable. Apply integer programming to express $b = 1 \leftrightarrow x \ge3$ My work: \begin{equation} \begin{cases} \...
0
votes
0answers
31 views

Valid parenthesis Matching in MSO

What is the Monodic Second Order formula that encodes all binary strings that represent a valid parenthesis matching ? By this I mean 1s represent '(' and 0s represent ')' and at every position, ...
3
votes
1answer
69 views

Encoding first order formula (or its tree) into binary string?

How to encode a first order formula into binary string, which I could give as input to Turing machine or program to do something with it (deciding is it satisfiable, or is concrete structure model for ...
2
votes
1answer
152 views

Simplifying this Boolean Expression

I have to simplify A+C'+B'CD but I don't see how. I had to deduce the expression starting from a logic diagram in which two AND gates were used for the B'CD part. Seeing the diagram all I can think ...
1
vote
2answers
125 views

Expressing the condition as a set of linear constraints

Express the condition "$x = 0$ if and only if $y = 0$" as a set of linear constraints, where $x,y$ are integers such that $ - 5 \le x \le 8$ and $0 \le y \le 1$
3
votes
0answers
65 views

Construct skolemform of: $\forall X.((\forall Y.\exists Z. R(X,Y,Z)) \land \forall S. \exists T. R(X, S,T))$

This question is not asking for a solution, but rather as a check / validation of my thought process. Given the form: $W = \forall X.((\forall Y.\exists Z. R(X,Y,Z)) \land \forall S. \exists T. R(X,...