pathterminuspages/brkmnd.dk/aboutcontactabout me

Øvelser 1.2.2

[Datalogi/Logic in Computer Science (Huth,Ryan)/Kapitel 1]

For følgende: vis hvilke der er valide, og hvilke der ikke er.

De er løst i Coq.

Require Import Classical. Variables p q r s t u : Prop. (* a *) Lemma LEMa : p \/ ~p. tauto. Qed. Goal (~p -> ~q) -> q -> p. intro H. intro H0. assert (p \/ ~p). apply LEMa. destruct H1. exact H1. absurd q. apply H. exact H1. exact H0. (* b *) Goal ~p \/ ~q -> ~(p /\ q). intro H. intro. destruct H. absurd p. exact H. apply H0. absurd q. exact H. apply H0. (* c *) Goal ~p -> p \/ q -> q. intro H. intro H0. destruct H0. absurd p. exact H. exact H0. exact H0. (* d *) Goal p \/ q -> ~q \/ r -> p \/ r. intro H. intro H0. destruct H. left. exact H. destruct H0. absurd q. exact H0. exact H. right. exact H0. (* e - Uden brug af MT *) Goal (p -> (q \/ r)) -> ~q -> ~r -> ~p. intro H. intro H0. intro H1. intro. assert (q \/ r). apply H. exact H2. destruct H3. absurd q. exact H0. exact H3. absurd r. exact H1. exact H3. (* f *) Goal ~p /\ ~q -> ~(p \/ q). intro H. intro. destruct H0. absurd p. apply H. exact H0. absurd q. apply H. exact H0. (* g *) Lemma ABSg : p /\ ~p -> False. intro H. absurd p. apply H. apply H. Qed. Goal p /\ ~p -> ~(r -> q) /\ (r -> q). intro H. assert (False). apply ABSg. apply H. exfalso. exact H0. (* h *) (* Da q kun kan hentes med p, og t kun kan hentes med s, kan følgen ikke bevises. *) Goal (p -> q) -> (s -> t) -> p \/ s -> q /\ t. (* i *) Lemma PBCi : (~p -> False) -> p. tauto. Qed. Goal ~(~p \/ q) -> p. intro H. apply PBCi. intro H0. absurd (~p \/ q). exact H. left. exact H0.
CommentsGuest Name:Comment: