Stack Overflow
Stack Overflow

Questions tagged [implication]

Anything related to the logical implication operation, i.e. a binary operation between two truth values A and B that in math is denoted by an arrow `A -> B` (A implies B) and that can be expressed in term of basic logical operations as `not A or B`.

Anything related to the logical implication operation, i.e. a binary operation between two truth values A and B that in math is denoted by an arrow A → B (A implies B) and that can be expressed in term of basic logical operations as not A or B.

29 questions
22
votes
8 answers

Is there an implication logical operator in python?

I would like to write a statement in python with logical implication. Something like: if x => y: do_sth() Of course, I know I could use: if (x and y) or not x: do_sth() But is there a logical operator for this in python?
running.t
  • 5,329
  • 3
  • 32
  • 50
9
votes
9 answers

P implies Q, how to read in english

how to read P implies Q in classical logic? example : Distributivity: Ka(X->Y) -> (KaX -> KaY) This is modal logic which uses classical logic rules. KaX : a knows the that X is true. I m curious about how to read implication in english? if…
DarthVader
  • 52,984
  • 76
  • 209
  • 300
6
votes
2 answers

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), ... and many people try to condense this…
Name McChange
  • 2,750
  • 5
  • 27
  • 46
6
votes
2 answers

Is this relationship between forall and exists provable in Coq/intuitionistic logic?

Is the following theorem provable in Coq? And if not, is there a way to prove it isn't provable? Theorem not_for_all_is_exists: forall (X : Set) (P : X -> Prop), ~(forall x : X, ~ P x) -> (exists x: X, P x). I know this related relationship is…
Others
  • 2,876
  • 2
  • 30
  • 52
5
votes
2 answers

SystemVerilog: implies operator vs. |->

Recently the question came up what the difference is between the usual implication operator (|->) and the implies operator in SystemVerilog. Unfortunately I couldn't find a clear answer yet. However, I collected the following information: From…
sebs
  • 205
  • 3
  • 9
4
votes
1 answer

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 speaking, meta level implication should be used to separate…
Gergely
  • 6,879
  • 6
  • 25
  • 35
3
votes
1 answer

Implication Graph Assignment

An implication graph is a directed graph where each node is assigned either true or false and any edge u -> v implies that if u is true then v is true. I know a straightforward O(n^2) algorithm to find an assignment in a general implication graph…
Corei13
  • 401
  • 2
  • 9
2
votes
1 answer

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 propositions and simply handle all 8 possibilities with reflexivity.…
OrenIshShalom
  • 5,974
  • 9
  • 37
  • 87
2
votes
1 answer

How would one prove ((p ⇒ q) ⇒ p) ⇒ p, using the Fitch system

FYI, the logic program I use cannot do contradiction introductions. This point is most likely irrelevant, for I highly doubt I would need to use any form of contradiction for this proof. In my attempt to solve this, I started off with assuming (p ⇒…
God's Drunkest Driver
  • 135
  • 9
2
votes
1 answer

Haskell - Use induction to prove an implication

I've to prove by induction that no f xs ==> null (filter f xs) Where : filter p [] = [] filter p (x:xs) | p x = x : filter p xs | otherwise = filter p xs null [] = True; null _ = False no p [] = True no p (x:xs) | p x = False …
Fossa
  • 159
  • 1
  • 6
2
votes
1 answer

how to code implication/equivalence in java

Hello i am a beginner in coding the logic with java , So i wanted to know how can i code the following information. i have these variables in a file presented like following example: my file.txt 5 1 4 6 2 3 the numbers actually represent…
user3136450
  • 31
  • 1
  • 4
1
vote
1 answer

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 going to need c somewhere. And I know how to prove b from a,…
markasoftware
  • 12,292
  • 8
  • 41
  • 69
1
vote
1 answer

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 trying to create an Ltac script that codifies the…
Landon D. C. Elkind
  • 23
  • 5
1
vote
1 answer

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) :- % A,B -> As,Bs list_to_ord_set(A,As), % A->As …
David Tonhofer
  • 14,559
  • 5
  • 55
  • 51
1
vote
1 answer

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 and U_d are binary decision variables: Y_i_d =…
k.agnes
  • 11
  • 1
1
2