28 questions
- Bountied 0
- Unanswered
- Frequent
- Score
- Trending
- Week
- Month
- Unanswered (my tags)
0
votes
1
answer
109
views
How to simplify these clauses into implications for an implication graph?
For a uni project I have to create an implication graph from clauses.
For example, from the clause (a or b), I can determine these implication :
¬a -> b
¬b -> a
but I really can't find the ...
0
votes
2
answers
79
views
How make to correctly logical implication in CP's Cplex
I'm new to CPLEX, and I'm doing a project using CP.
I have a multilist A that has 4 arguments : one Operation o, one Surgeon s, one Room r and one Time t
A[o,s,r,t] == 1 if and only if the operation ...
1
vote
1
answer
470
views
How to break up an implication into two subgoals in Coq?
Say I have the following:
Lemma my_lemma :
forall a b c,
a -> (b -> c) -> d.
Proof.
intros.
Then, above the line, I get:
X : a
X0 : b -> c
Let's say that in my proof, I know I'm ...
0
votes
1
answer
239
views
Material Conditional and Equivalence in Programming
I have just started reading into propositional calculus/logic, and have realised that a lot of the foundational concepts in this area are similar to those encountered in programming. That is, ...
0
votes
2
answers
392
views
How to linearize an implication?
Could someone help me linearize this implication?
Being x and y integer variables, the implication is the following
x >= 1 --> y = 0
y >= 1 --> x = 0
I would really appreciate some help.
0
votes
1
answer
948
views
What is the difference between the symbol '->' and '|->' in System Verilog Assertion Properties
I have encountered an example property which works here:
property p_a;
@(posedge clk) $rose(a) -> $rose(b);
endproperty
There is no syntax error above.
Then I tried to modify to this
property ...
1
vote
1
answer
155
views
Coq: Ltac for transitivity of implication (a.k.a. hypothetical syllogism)
This question is about a project that I am doing, namely, to code Principia Mathematica in Coq. Principia has derived rules of inference, one of which is Syll:
∀ P Q R : Prop,
P→Q, Q→R : P→R
I am ...
1
vote
1
answer
59
views
Implication branch doesn't see variables
Here is a little test:
:- begin_tests(tuturuu).
test(foo) :- Expected=[a,b],Got=[a,b,c],verdict(foo,Expected,Got).
% helper: transform lists A,B into ordered sets As,Bs
setify(A,B,As,Bs) :- % ...
4
votes
1
answer
295
views
Object level implication in Isabelle/HOL
I see that many theorems in Isabelle/HOL prefer meta-level implication:
==>
instead of
-->
the object logic level, i.e. higher order logic implication.
Isabelle wiki says that roughly ...
1
vote
1
answer
79
views
Implementing an implication where the LHS is not a binary?
Trying to implement and indicator constraint in Python + Gurobi where the indicator(LHS) is a sum of a binary decision variable.
Hi, I've would like to implement following in Python + Gurobi:
Y_i_d ...
2
votes
1
answer
820
views
Transitivity of -> in Coq
I'm trying to prove the transitivity of -> in Coq's propositions:
Theorem implies_trans : forall P Q R : Prop,
(P -> Q) -> (Q -> R) -> (P -> R).
Proof.
I wanted to destruct all ...
7
votes
2
answers
1k
views
Prolog if-then-else constructs: -> vs *-> vs. if_/3
As noted in another StackOverflow answer that I can't seem to find anymore, this pattern emerges frequently in practical Prolog code:
pred(X) :-
guard(X),
...
pred(X) :-
\+ guard(X),
....
-1
votes
1
answer
2k
views
Logical Equivalence: Show that R OR P implies R OR Q is equivalent to NOT R implies (P implies Q)?
I'm practicing logical equivalence and I've come across a question that I'm struggling to answer:
Show that (R or P -> R or Q) is equivalent to (not R -> (P -> Q)).
I've examined the truth tables of ...
-4
votes
1
answer
1k
views
Prolog - a predicate to compare three arguments
I am new into prolog and I've already done some coding, but I have a task I cannot handle. Could you please tell me how to describe a working predicate, that compares arg1, arg2 and arg3 and returns ...
0
votes
1
answer
111
views
Checking if a column has a certain value, then restrict another by a list
I am wondering if there is any way for me to check if a column has a value, if the value is XXXXX then another column must be in the list of (A,B,C).
something like:
CREATE TABLE test (a CHAR(60),b ...