jp-diegidio

(** * Cantor's diagonal argument (in Rocq)

  We go for the simplest construction, which is not
  in terms of sets, just (type-theoretic) *functions*
  plus the most basic functional extensionality, i.e.
  eta-equivalence/conversion.

  TODO:
  - The proof could probably be cleaner,
    and the overall assumptions made clearer.

jp-diegidio

/*	gentzen / gentzen.pl v0.10.30-alpha
	A constructive logic solver in Prolog
	Copyright (C) 2024 Julio P. Di Egidio
	http://julio.diegidio.name
	This software is released under GNU-GPLv3+.
	As usual, NO WARRANTY OF ANY KIND is implied.
	
	At this stage, implements up to a solver for
	affine intuitionistic propositional logic, with
	support for classical via negative translation.

jp-diegidio

/*	pairwise (pairwise.pl) v1.1.0-alpha
	Pairwise intersection solver in Prolog
	Copyright (C) 2024 Julio P. Di Egidio
	http://julio.diegidio.name
	This software is released in the Public Domain.
	As usual, NO WARRANTY OF ANY KIND is implied.
	
	Implements a (tentative) solution to the question:
	"Minimum number of elements in all sets" - StackExchange
	Question: https://puzzling.stackexchange.com/questions/128961

jp-diegidio

(** Epimenides' Paradox (v1.4-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
      "all Cretans are liars!"
  Question:

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 GNU-GPLv3+.
	As usual, NO WARRANTY OF ANY KIND is implied.
*/

% Developed and tested on:
% - GNU Prolog 1.5.0 (64 bits)

jp-diegidio

(** Exercise Zulip-01

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

Was <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
--------------------------