Documentation

Linglib.Core.Logic.TweetyNixon

Tweety Triangle and Nixon Diamond #

[Vel96] [GP96] [AP12]

The two classic default-reasoning testbeds, as finite world types shared by the rival accounts in Studies/Veltman1996, Studies/GoldszmidtPearl1996, and Studies/AsherPelletier2013:

  1. Tweety Triangle (specificity): birds normally fly; penguins are birds; penguins normally don't fly. The more specific default wins.
  2. Nixon Diamond (conflicting defaults): Quakers are normally pacifist; Republicans are normally not; Nixon is both.

Main declarations #

source
inductive Core.Logic.TweetyNixon.TweetyWorld :
Type

The Tweety world: 4 possible states of an entity.

Instances For
    source
    @[implicit_reducible]
    instance Core.Logic.TweetyNixon.instDecidableEqTweetyWorld :
    DecidableEq TweetyWorld
    Equations
    source
    def Core.Logic.TweetyNixon.instReprTweetyWorld.repr :
    TweetyWorld → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Core.Logic.TweetyNixon.instReprTweetyWorld :
      Repr TweetyWorld
      Equations
      source
      @[implicit_reducible]
      instance Core.Logic.TweetyNixon.instFintypeTweetyWorld :
      Fintype TweetyWorld
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def Core.Logic.TweetyNixon.isBird :
      TweetyWorld → Prop
      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Core.Logic.TweetyNixon.instDecidablePredTweetyWorldIsBird :
        DecidablePred isBird
        Equations
        • One or more equations did not get rendered due to their size.
        source
        def Core.Logic.TweetyNixon.isPenguin :
        TweetyWorld → Prop
        Equations
        Instances For
          source
          @[implicit_reducible]
          instance Core.Logic.TweetyNixon.instDecidablePredTweetyWorldIsPenguin :
          DecidablePred isPenguin
          Equations
          • One or more equations did not get rendered due to their size.
          source
          def Core.Logic.TweetyNixon.flies :
          TweetyWorld → Prop
          Equations
          Instances For
            source
            @[implicit_reducible]
            instance Core.Logic.TweetyNixon.instDecidablePredTweetyWorldFlies :
            DecidablePred flies
            Equations
            • One or more equations did not get rendered due to their size.
            source
            theorem Core.Logic.TweetyNixon.penguin_is_bird (w : TweetyWorld) :
            isPenguin w → isBird w

            Every penguin is a bird.

            source
            inductive Core.Logic.TweetyNixon.NixonWorld :
            Type

            The Nixon world: 4 possible states.

            Instances For
              source
              @[implicit_reducible]
              instance Core.Logic.TweetyNixon.instDecidableEqNixonWorld :
              DecidableEq NixonWorld
              Equations
              source
              def Core.Logic.TweetyNixon.instReprNixonWorld.repr :
              NixonWorld → ℕ → Std.Format
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[implicit_reducible]
                instance Core.Logic.TweetyNixon.instReprNixonWorld :
                Repr NixonWorld
                Equations
                source
                def Core.Logic.TweetyNixon.isQuaker :
                NixonWorld → Prop
                Equations
                Instances For
                  source
                  def Core.Logic.TweetyNixon.isRepublican :
                  NixonWorld → Prop
                  Equations
                  Instances For
                    source
                    def Core.Logic.TweetyNixon.isPacifist :
                    NixonWorld → Prop
                    Equations
                    Instances For