This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/* | |
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. | |
*/ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** 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 := |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(** Grelling–Nelson Paradox. | |
Module [GnpLogic] is the basic logical analysis, | |
with the conclusion "phi is incomplete". | |
Module [GnpExtLogic] is the first attempt at extending | |
the logic, but fails to change the conclusion: indeed | |
it turns out rather indicative that the "paradox" holds | |
regardless of the specifics of [phi]: having the *type of* | |
[phi] in the context (IOW, that the class of such functions |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
% (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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/* | |
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
/* | |
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 | |
-------------------------- |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
/* | |
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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
% (SWI-Prolog) | |
:- use_module(library(clpfd)). | |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
%! sudoku(?Rows) is nondet. | |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% | |
sudoku(Rows) :- | |
sudoku__rows(Rows), | |
sudoku__cols(Rows), |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/* --------------------------------------------------------------------------- | |
How to calculate this probability? | |
Originally from a question by "Houwu Chen": | |
https://groups.google.com/d/msg/sci.math/YgvVT-SLvRg/RLn2agzZM7kJ | |
https://groups.google.com/d/msg/sci.math/YgvVT-SLvRg/2TC-NcV-AqoJ | |
UPDATED 2015-04-27: Fixed a bug in to_digit_probs__do/4. | |
Question: |