jp-diegidio

(**
  Epimenides' Paradox (v1.3-draft)

  << 'Morning everybody,
     "Epimenides lies iff everybody lies!" which
     I am taking to be *the predicative version of*
     "the uncooperative rational player". >>

  Proposition:
    Epimenides the Cretan says

jp-diegidio

From Coq Require Import Bool.

Ltac solve_sat_naive :=
  repeat multimatch goal with
  | [|- exists _ : bool, _] => exists true
  | [|- exists _ : bool, _] => exists false
  end; reflexivity.

Example ex_01 : exists x y, x && negb y = true.
Proof. solve_sat_naive. Qed.

jp-diegidio

/*
  prime_gen (prime_gen.pl) v1.0.0-rc
  Simple prime number generation in Prolog
  Copyright (C) 2023 Julio P. Di Egidio
  http://julio.diegidio.name
  
  This software is released under the GNU-GPLv3 license.
  
  As usual, NO WARRANTY OF ANY KIND is implied.
*/

jp-diegidio

(** Exercise Zulip-01

"Prove, by induction on boolean terms, that one step of
evaluation in this lambda calculus reduces the term size."

<https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Tactic.20for.20destructing.20specific.20pattern.20match.20in.20Goal/near/394101120>

*)

Inductive term : Type :=

jp-diegidio

(** Grelling-Nelson Paradox.

  Module [GnpLogic] is the basic logical analysis,
  with the conclusion "phi is incomplete": where,
  together with a notion of *functional extensionality*
  (represented by [peq]), that [phi] is a *total function*
  seems all it takes for the "paradox" to apply.

  Module [GnpExtLogic] is the first attempt at extending
  the logic by extending the domain of discourse, but fails

jp-diegidio

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% (SWI-Prolog 7.5.1)

:- module(ilog2,
    [   %%
        ilog2_n/3,      % +X, -Y, -C
        ilog2_b/3,      % +X, -Y, -C
        ilog2_i/3,      % +X, -Y, -C
        %ilog2_f/3,      % +X, -Y, -C

jp-diegidio

/*
Einstein's riddle: who owns the fish?

There are 5 houses in 5 different colors in a row. In each house lives a
person with a different nationality. The 5 owners drink a certain type of
beverage, smoke a certain brand of cigar, and keep a certain pet. No
owners have the same pet, smoke the same brand of cigar, or drink the same
beverage. Other facts:

1. The Brit lives in the red house.

jp-diegidio

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/*
Answer Sources in Prolog (SWI) - Preview
Answer Sources: Extensions
Copyright (c) 2015 Julio P. Di Egidio
http://julio.diegidio.name/
All rights reserved.

Answer Sources: Extensions
--------------------------

jp-diegidio

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
/*

How few candies does the teacher need?
--------------------------------------

Problem:
Alice is a teacher of kindergarten. She wants to give some candies to
the children in her class. All the children sit in a line and each of
them has a rating score according to his or her usual performance.

jp-diegidio

% (SWI-Prolog)
:- use_module(library(clpfd)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%!	sudoku(?Rows) is nondet.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

sudoku(Rows) :-
	sudoku__rows(Rows),
	sudoku__cols(Rows),