Diffusion afp-devel 1e0f664cffc8

merge from afp-2021-1
1e0f664cffc8
Actions

Tags

None

Subscribers

None

Description

merge from afp-2021-1

Details

Provenance

Fabian Huch <huch@in.tum.de>

Authored on

Parents

rAFP6631e28c5f5f: regenerate site;
rAFP255dda6d93dc: Improvements.

Branches

Unknown

Tags

Unknown

Event Timeline

Fabian Huch <huch@in.tum.de> committed rAFP1e0f664cffc8: merge from afp-2021-1.Jul 7 2022, 5:24 PM

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.

255dda6d93dc Improvements.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
e68b946939fa tuned
Author
florian.haftmann
Browse Repository
No Builds
No Audits
521e4864b960 removed more material now residing in distribution
Author
florian.haftmann
Browse Repository
No Builds
No Audits
01df7496c94e separated non-computable instance of bit comprehension from computable one
Author
florian.haftmann
Browse Repository
No Builds
No Audits
e583d7f737be Small changes.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
5333b8ad7d60 Undo accidental changes.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
dec6b76379ea Tuned.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
5e3a947f603c tuned -- follow clone in $ISABELLE_HOME/src/HOL/Imperative_HOL/Heap_Monad.thy;
Author
makarius
Browse Repository
No Builds
No Audits
459c3312f115 minor performance tuning: avoid redundant BigInt construction;
Author
makarius
Browse Repository
No Builds
No Audits
cfb6849889bb prefer self-made Array.T, to avoid problems with ArraySeq in Scala 3;
Author
makarius
Browse Repository
No Builds
No Audits
18281e769389 more robust Array.T for Scala 2.13 and 3.x, following Isabelle/ca450d902198;
Author
makarius
Browse Repository
No Builds
No Audits
b48c96946723 Move code lemmas for symbolic computation of bit operations on int to…
Author
florian.haftmann
Browse Repository
No Builds
No Audits
4e7b90c36883 renamings
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
cdb3cf2b0a3c Relational_Disjoint_Set_Forests: improved abstractions
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
d9db5956fd1a Simplified a proof using Cauchy–Schwarz
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
79e09cd07d73 removed precondition in det_four_block_mat
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
f0ff48f384e9 merge
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
142c851d4abc removed assumption in det_bound_hadamard_tight, moved some basic lemmas on…
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
7b49c265e0fe merge from afp-2021-1
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
365c3d8497ce renamed det_bound_gram to det_bound_hadamard, showed that bound is tight (using…
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
e2545be0714b added lemma for special case of small integer solutions (no mixed integer)…
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
6927929601ba document change in metadata
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
6cf62d8e618e generalized fixed bounds on determinants to predicate; added an improved…
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
52a3cc9ded7d Code generated in the same directory
Author
mohammadabdulaziz
Browse Repository
No Builds
No Audits
54aa4793df33 Removed ML code from AFP entry
Author
mohammadabdulaziz
Browse Repository
No Builds
No Audits
0f9739670445 adapted to scala-3.1.2;
Author
makarius
Browse Repository
No Builds
No Audits
2c63017ece34 merge from afp-2021-1
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9c49b55d7a1f merged
Author
desharna
Browse Repository
No Builds
No Audits
d2ca17e8b6e2 replaced IMGU by min_IMGU
Author
desharna
Browse Repository
No Builds
No Audits
ecba8ab471bb replaced MGU by IMGU
Author
desharna
Browse Repository
No Builds
No Audits
5b3fb77e044f exposed that inverse of renaming only maps variables to variables
Author
desharna
Browse Repository
No Builds
No Audits
0f47c7a36c6d added the r{n..} regular expression to the extensions directory in the Posix…
Author
Christian Urban <christian.urban@kcl.ac.uk>
Browse Repository
No Builds
No Audits
b8bf214bae37 merge from afp-2021-1
Author
kleing
Browse Repository
No Builds
No Audits
12de1f883dc0 tuned efficiency of XML parser
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
ae47c479a7c4 tuned
Author
Christian Urban <christian.urban@kcl.ac.uk>
Browse Repository
No Builds
No Audits
66e3dcab868b updated the abstract in root.tex
Author
Christian Urban <christian.urban@kcl.ac.uk>
Browse Repository
No Builds
No Audits
09f66a4ada38 added the r{..n} regular expression to the extensions directory
Author
Christian Urban <christian.urban@kcl.ac.uk>
Browse Repository
No Builds
No Audits
969d123ac0b9 merged
Author
traytel
Browse Repository
No Builds
No Audits
2500a913c1f2 tuned BNF bound
Author
traytel
Browse Repository
No Builds
No Audits
5b2658c54443 strict bounds for BNFs (by Jan van Brügge)
Author
traytel
Browse Repository
No Builds
No Audits
bee741e8e528 merge from afp-2021-1 (replaying devel commit)
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
3f502f9f9cc7 replaced python RAKE component with Isabelle/Scala Rake component;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
f8a002855e5e merged
Author
makarius
Browse Repository
No Builds
No Audits
4968f5a0b474 avoid hardwired pdf;
Author
makarius
Browse Repository
No Builds
No Audits
256787b32958 adapted to Isabelle/986506233812;
Author
makarius
Browse Repository
No Builds
No Audits
c7498ca83836 merged
Author
Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
Browse Repository
No Builds
No Audits
803497c3eac5 added an implementation of pseudo remainder sequences for calculating Tarski…
Author
Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
Browse Repository
No Builds
No Audits
0d159a7589cb merged
Author
desharna
Browse Repository
No Builds
No Audits
221e9df71dbb updated to Isabelle/3c544d64c218
Author
desharna
Browse Repository
No Builds
No Audits
574ddb031262 merge from afp-2021-1
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits

Changes (728)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

admin/

site/

themes/

afp/

layouts/

entries/

shortcodes/

statistics.html

Boolos_Curious_Inference.toml

Boolos_Curious_Inference

tools/

afp_site_gen.scala

data/

ADS_Functor.html

AI_Planning_Languages_Semantics.html

Abortable_Linearizable_Modules.html

Abs_Int_ITP2012.html

Abstract-Hoare-Logics.html

Abstract-Rewriting.html

Abstract_Completeness.html

Abstract_Soundness.html

Ackermanns_not_PR.html

Actuarial_Mathematics.html

Adaptive_State_Counting.html

Affine_Arithmetic.html

Aggregation_Algebras.html

Akra_Bazzi.html

Algebraic_Numbers.html

Algebraic_VCs.html

Allen_Calculus.html

Amicable_Numbers.html

Amortized_Complexity.html

Applicative_Lifting.html

Approximation_Algorithms.html

Architectural_Design_Patterns.html

Aristotles_Assertoric_Syllogistic.html

Arith_Prog_Rel_Primes.html

ArrowImpossibilityGS.html

Attack_Trees.html

Auto2_Imperative_HOL.html

AutoFocus-Stream.html

Automated_Stateful_Protocol_Verification.html

Automatic_Refinement.html

AxiomaticCategoryTheory.html

BD_Security_Compositional.html

BNF_Operations.html

Banach_Steinhaus.html

Belief_Revision.html

Bell_Numbers_Spivey.html

BenOr_Kozen_Reif.html

Berlekamp_Zassenhaus.html

Bertrands_Postulate.html

Bicategory.html

BinarySearchTree.html

Binding_Syntax_Theory.html

Binomial-Heaps.html

Binomial-Queues.html

Boolean_Expression_Checkers.html

Boolos_Curious_Inference.html

Bounded_Deducibility_Security.html

Buchi_Complementation.html

Budan_Fourier.html

Buffons_Needle.html

BytecodeLogicJmlTypes.html

C2KA_DistributedSystems.html

CAVA_Automata.html

CAVA_LTL_Modelchecker.html

CISC-Kernel.html

CZH_Elementary_Categories.html

CZH_Foundations.html

CZH_Universal_Constructions.html

CakeML_Codegen.html

Call_Arity.html

Card_Equiv_Relations.html

Card_Multisets.html

Card_Number_Partitions.html

Card_Partitions.html

Case_Labeling.html

Catalan_Numbers.html

Cayley_Hamilton.html

Certification_Monads.html

Chandy_Lamport.html

Chord_Segments.html

Clique_and_Monotone_Circuits.html

ClockSynchInst.html

Closest_Pair_Points.html

Coinductive.html

Coinductive_Languages.html

Collections.html

Combinable_Wands.html

Combinatorics_Words.html

Combinatorics_Words_Graph_Lemma.html

Combinatorics_Words_Lyndon.html

Comparison_Sort_Lower_Bound.html

Compiling-Exceptions-Correctly.html

Complete_Non_Orders.html

Completeness.html

Complex_Bounded_Operators.html

Complex_Geometry.html

ComponentDependencies.html

ConcurrentGC.html

ConcurrentIMP.html

Concurrent_Ref_Alg.html

Concurrent_Revisions.html

Conditional_Simplification.html

Conditional_Transfer_Rule.html

Consensus_Refined.html

Constructive_Cryptography.html

Constructive_Cryptography_CM.html

Constructor_Funs.html

Containers.html

Core_SC_DOM.html

Correctness_Algebras.html

Cotangent_PFD_Formula.html

Count_Complex_Roots.html

CryptoBasedCompositionalProperties.html

Cubic_Quartic_Equations.html

DFS_Framework.html

DOM_Components.html

DPRM_Theorem.html

DPT-SAT-Solver.html

DataRefinementIBP.html

Datatype_Order_Generator.html

Decl_Sem_Fun_PL.html

Decreasing-Diagrams-II.html

Decreasing-Diagrams.html

Dedekind_Real.html

Deep_Learning.html

Delta_System_Lemma.html

Density_Compiler.html

Dependent_SIFUM_Refinement.html

Dependent_SIFUM_Type_Systems.html

Depth-First-Search.html

Derangements.html

Descartes_Sign_Rule.html

Design_Theory.html

Dict_Construction.html

Differential_Dynamic_Logic.html

Differential_Game_Logic.html

Digit_Expansions.html

Dijkstra_Shortest_Path.html

Diophantine_Eqns_Lin_Hom.html

Dirichlet_L.html

Dirichlet_Series.html

DiscretePricing.html

Discrete_Summation.html

Dominance_CHK.html

DynamicArchitectures.html

Dynamic_Tables.html

E_Transcendental.html

Echelon_Form.html

EdmondsKarp_Maxflow.html

Efficient-Mergesort.html

Elliptic_Curves_Group_Law.html

Encodability_Process_Calculi.html

Epistemic_Logic.html

Equivalence_Relation_Enumeration.html

Ergodic_Theory.html

Error_Function.html

Euler_MacLaurin.html

Euler_Partition.html

Extended_Finite_State_Machine_Inference.html

Extended_Finite_State_Machines.html

FOL-Fitting.html

FOL_Axiomatic.html

FOL_Harrison.html

FOL_Seq_Calc1.html

FOL_Seq_Calc2.html

FOL_Seq_Calc3.html

FO_Theory_Rewriting.html

Factor_Algebraic_Polynomial.html

Factored_Transition_System_Bounding.html

Falling_Factorial_Sum.html

FeatherweightJava.html

Featherweight_OCL.html

FileRefinement.html

Finger-Trees.html

Finite-Map-Extras.html

Finite_Automata_HF.html

Finite_Fields.html

Finitely_Generated_Abelian_Groups.html

First_Order_Terms.html

First_Welfare_Theorem.html

Fishburn_Impossibility.html

Fisher_Yates.html

Fishers_Inequality.html

Flow_Networks.html

Floyd_Warshall.html

Flyspeck-Tame.html

FocusStreamsCaseStudies.html

Formal_Puiseux_Series.html

Formal_SSA.html

Formula_Derivatives.html

Foundation_of_geometry.html

Free-Boolean-Algebra.html

Free-Groups.html

Frequency_Moments.html

Fresh_Identifiers.html

FunWithFunctions.html

FunWithTilings.html

Functional-Automata.html

Functional_Ordered_Resolution_Prover.html

Furstenberg_Topology.html

GPU_Kernel_PL.html

GaleStewart_Games.html

Gale_Shapley.html

Game_Based_Crypto.html

Gauss-Jordan-Elim-Fun.html

Gauss_Jordan.html

Gauss_Sums.html

Gaussian_Integers.html

General-Triangle.html

Generalized_Counting_Sort.html

Generic_Deriving.html

Generic_Join.html

GewirthPGCProof.html

Girth_Chromatic.html

Goedel_HFSet_Semantic.html

Goedel_HFSet_Semanticless.html

Goedel_Incompleteness.html

Goodstein_Lambda.html

GraphMarkingIBP.html

Graph_Saturation.html

Graph_Theory.html

Groebner_Bases.html

Groebner_Macaulay.html

Gromov_Hyperbolicity.html

Grothendieck_Schemes.html

Group-Ring-Module.html

HOLCF-Prelude.html

HRB-Slicing.html

Hahn_Jordan_Decomposition.html

Hello_World.html

HereditarilyFinite.html

Hermite_Lindemann.html

Hidden_Markov_Models.html

Higher_Order_Terms.html

Hoare_Time.html

Hood_Melville_Queue.html

HotelKeyCards.html

Hybrid_Logic.html

Hybrid_Multi_Lane_Spatial_Logic.html

Hybrid_Systems_VCs.html

IEEE_Floating_Point.html

IFC_Tracking.html

IMP2_Binary_Heap.html

IMP_Compiler.html

IP_Addresses.html

Imperative_Insertion_Sort.html

Impossible_Geometry.html

Incompleteness.html

Incredible_Proof_Machine.html

Independence_CH.html

Inductive_Confidentiality.html

Inductive_Inference.html

InfPathElimination.html

InformationFlowSlicing.html

InformationFlowSlicing_Inter.html

Integration.html

Interpolation_Polynomials_HOL_Algebra.html

Interpreter_Optimizations.html

Interval_Arithmetic_Word32.html

Intro_Dest_Elim.html

Iptables_Semantics.html

Irrational_Series_Erdos_Straus.html

Irrationality_J_Hancl.html

Irrationals_From_THEBOOK.html

Isabelle_C.html

Isabelle_Marries_Dirac.html

Isabelle_Meta_Model.html

Jacobson_Basic_Algebra.html

JinjaThreads.html

JiveDataStoreModel.html

Jordan_Hoelder.html

Jordan_Normal_Form.html

KAT_and_DRA.html

Key_Agreement_Strong_Adversaries.html

Kleene_Algebra.html

Knights_Tour.html

Knot_Theory.html

Knuth_Bendix_Order.html

Knuth_Morris_Pratt.html

Koenigsberg_Friendship.html

Kuratowski_Closure_Complement.html

LLL_Basis_Reduction.html

LLL_Factorization.html

LP_Duality.html

LTL_Master_Theorem.html

LTL_Normal_Form.html

LTL_to_DRA.html

LTL_to_GBA.html

Lam-ml-Normalization.html

LambdaAuth.html

Lambda_Free_EPO.html

Lambda_Free_KBOs.html

Lambda_Free_RPOs.html

Landau_Symbols.html

Laplace_Transform.html

Latin_Square.html

LatticeProperties.html

Launchbury.html

Laws_of_Large_Numbers.html

Lazy-Lists-II.html

Lifting_Definition_Option.html

Lifting_the_Exponent.html

LightweightJava.html

LinearQuantifierElim.html

Linear_Inequalities.html

Linear_Programming.html

Linear_Recurrences.html

Liouville_Numbers.html

List-Index.html

List-Infinite.html

List_Interleaving.html

List_Inversions.html

List_Update.html

LocalLexing.html

Localization_Ring.html

Locally-Nameless-Sigma.html

Logging_Independent_Anonymity.html

Lowe_Ontological_Argument.html

Lower_Semicontinuous.html

Lucas_Theorem.html

MDP-Algorithms.html

MDP-Rewards.html

MFMC_Countable.html

MFODL_Monitor_Optimized.html

MFOTL_Monitor.html

MSO_Regex_Equivalence.html

Markov_Models.html

Mason_Stothers.html

Matrices_for_ODEs.html

Matrix_Tensor.html

Max-Card-Matching.html

Median_Method.html

Median_Of_Medians_Selection.html

Mersenne_Primes.html

Metalogic_ProofChecker.html

Minimal_SSA.html

Minkowskis_Theorem.html

Minsky_Machines.html

Modal_Logics_for_NTS.html

Modular_Assembly_Kit_Security.html

Modular_arithmetic_LLL_and_HNF_algorithms.html

Monad_Memo_DP.html

Monad_Normalisation.html

MonoBoolTranAlgebra.html

MonoidalCategory.html

Monomorphic_Monad.html

MuchAdoAboutTwo.html

Multi_Party_Computation.html

Multirelations.html

Multiset_Ordering_NPC.html

Myhill-Nerode.html

Name_Carrying_Type_Inference.html

Nash_Williams.html

Nat-Interval-Logic.html

Native_Word.html

Nested_Multisets_Ordinals.html

Network_Security_Policy_Verification.html

Neumann_Morgenstern_Utility.html

No_FTL_observers.html

Noninterference_CSP.html

Noninterference_Concurrent_Composition.html

Noninterference_Generic_Unwinding.html

Noninterference_Inductive_Unwinding.html

Noninterference_Ipurge_Unwinding.html

Noninterference_Sequential_Composition.html

NormByEval.html

Nullstellensatz.html

Open_Induction.html

Optimal_BST.html

Orbit_Stabiliser.html

Order_Lattice_Props.html

Ordered_Resolution_Prover.html

Ordinal_Partitions.html

Ordinals_and_Cardinals.html

Ordinary_Differential_Equations.html

PAC_Checker.html

POPLmark-deBruijn.html

PSemigroupsConvolution.html

Package_logic.html

Padic_Ints.html

Pairing_Heap.html

Paraconsistency.html

Parity_Game.html

Partial_Function_MR.html

Partial_Order_Reduction.html

Password_Authentication_Protocol.html

Perfect-Number-Thm.html

Perron_Frobenius.html

Physical_Quantities.html

Pi_Calculus.html

Pi_Transcendental.html

Planarity_Certificates.html

Pluennecke_Ruzsa_Inequality.html

Poincare_Bendixson.html

Poincare_Disc.html

Polynomial_Factorization.html

Polynomial_Interpolation.html

Polynomials.html

Pop_Refinement.html

Posix-Lexing.html

Possibilistic_Noninterference.html

Power_Sum_Polynomials.html

Pratt_Certificate.html

Prefix_Free_Code_Combinators.html

Presburger-Automata.html

Prim_Dijkstra_Simple.html

Prime_Distribution_Elementary.html

Prime_Harmonic_Series.html

Prime_Number_Theorem.html

Priority_Queue_Braun.html

Priority_Search_Trees.html

Probabilistic_Noninterference.html

Probabilistic_Prime_Tests.html

Probabilistic_System_Zoo.html

Probabilistic_Timed_Automata.html

Probabilistic_While.html

Program-Conflict-Analysis.html

Progress_Tracking.html

Projective_Geometry.html

Projective_Measurements.html

Proof_Strategy_Language.html

Propositional_Proof_Systems.html

Prpu_Maxflow.html

PseudoHoops.html

Psi_Calculi.html

Ptolemys_Theorem.html

Public_Announcement_Logic.html

QR_Decomposition.html

Quasi_Borel_Spaces.html

Quaternions.html

Quick_Sort_Cost.html

RIPEMD-160-SPARK.html

Ramsey-Infinite.html

Random_BSTs.html

Random_Graph_Subgraph_Threshold.html

Randomised_BSTs.html

Randomised_Social_Choice.html

Rank_Nullity_Theorem.html

Real_Power.html

Real_Time_Deque.html

Recursion-Addition.html

Recursion-Theory-I.html

Refine_Imperative_HOL.html

Refine_Monadic.html

RefinementReactive.html

Regex_Equivalence.html

Regression_Test_Selection.html

Regular-Sets.html

Regular_Algebras.html

Regular_Tree_Relations.html

Relation_Algebra.html

Relational-Incorrectness-Logic.html

Relational_Disjoint_Set_Forests.html

Relational_Forests.html

Relational_Method.html

Relational_Minimum_Spanning_Trees.html

Relational_Paths.html

Rep_Fin_Groups.html

ResiduatedTransitionSystem.html

Residuated_Lattices.html

Resolution_FOL.html

Rewrite_Properties_Reduction.html

Rewriting_Z.html

Ribbon_Proofs.html

Robbins-Conjecture.html

Robinson_Arithmetic.html

Root_Balanced_Tree.html

Roth_Arithmetic_Progressions.html

Roy_Floyd_Warshall.html

SATSolverVerification.html

SC_DOM_Components.html

SDS_Impossibility.html

SIFUM_Type_Systems.html

Safe_Distance.html

Saturation_Framework.html

Saturation_Framework_Extensions.html

Schutz_Spacetime.html

Secondary_Sylow.html

Security_Protocol_Refinement.html

Selection_Heap_Sort.html

SenSocialChoice.html

Separation_Algebra.html

Separation_Logic_Imperative_HOL.html

SequentInvertibility.html

Shadow_DOM.html

Shadow_SC_DOM.html

Shivers-CFA.html

ShortestPath.html

Sigma_Commit_Crypto.html

Signature_Groebner.html

Simple_Firewall.html

Simplicial_complexes_and_boolean_functions.html

SimplifiedOntologicalArgument.html

Skip_Lists.html

Sliding_Window_Algorithm.html

Smith_Normal_Form.html

Smooth_Manifolds.html

Sophomores_Dream.html

Sort_Encodings.html

Source_Coding_Theorem.html

Special_Function_Bounds.html

Splay_Tree.html

Sqrt_Babylonian.html

Stable_Matching.html

Statecharts.html

Stateful_Protocol_Composition_and_Typing.html

Stellar_Quorums.html

Stern_Brocot.html

Stewart_Apollonius.html

Stirling_Formula.html

Stochastic_Matrices.html

Stone_Algebras.html

Stone_Kleene_Relation_Algebras.html

Stone_Relation_Algebras.html

Store_Buffer_Reduction.html

Stream-Fusion.html

Stream_Fusion_Code.html

Strong_Security.html

Sturm_Sequences.html

Sturm_Tarski.html

Stuttering_Equivalence.html

Subresultants.html

Subset_Boolean_Algebras.html

SumSquares.html

Sunflowers.html

Surprise_Paradox.html

Symmetric_Polynomials.html

Syntax_Independent_Logic.html

Szemeredi_Regularity.html

TESL_Language.html

Tail_Recursive_Functions.html

Tarskis_Geometry.html

Taylor_Models.html

Three_Circles.html

Timed_Automata.html

Topological_Semantics.html

TortoiseHare.html

Transcendence_Series_Hancl_Rucki.html

Transformer_Semantics.html

Transition_Systems_and_Automata.html

Transitive-Closure-II.html

Transitive-Closure.html

Transitive_Models.html

Tree-Automata.html

Tree_Decomposition.html

Twelvefold_Way.html

Types_Tableaus_and_Goedels_God.html

Types_To_Sets_Extension.html

UPF_Firewall.html

Universal_Hash_Families.html

Universal_Turing_Machine.html

UpDown_Scheme.html

Van_Emde_Boas_Trees.html

Van_der_Waerden.html

VectorSpace.html

Verified-Prover.html

Verified_SAT_Based_AI_Planning.html

VerifyThis2018.html

VerifyThis2019.html

Vickrey_Clarke_Groves.html

Virtual_Substitution.html

VolpanoSmith.html

WHATandWHERE_Security.html

WOOT_Strong_Eventual_Consistency.html

WebAssembly.html

Weight_Balanced_Trees.html

Weighted_Path_Order.html

Well_Quasi_Orders.html

Wetzels_Problem.html

Winding_Number_Eval.html

WorkerWrapper.html

X86_Semantics.html

Youngs_Inequality.html

ZFC_in_HOL.html

Zeta_3_Irrational.html

Zeta_Function.html

statistics/

boolos_curious_inference

word_lib/

topics/

logic/

philosophical-aspects/

rAFP1e0f664cffc8

admin/site/themes/afp/layouts/entries/single.html

admin/site/themes/afp/layouts/shortcodes/statistics.html

metadata/authors.toml

metadata/entries/Boolos_Curious_Inference.toml

thys/Boolos_Curious_Inference/Boo1.thy

thys/Boolos_Curious_Inference/Boo2.thy

thys/Boolos_Curious_Inference/ROOT

thys/Boolos_Curious_Inference/document/root.bib

thys/Boolos_Curious_Inference/document/root.tex

thys/ROOTS

tools/afp_site_gen.scala

web/authors/index.html

web/authors/index.json

web/authors/ketland/index.html

web/authors/ketland/index.xml

web/data/keywords.json

web/entries/ADS_Functor.html

web/entries/AI_Planning_Languages_Semantics.html

web/entries/AODV.html

web/entries/AVL-Trees.html

web/entries/AWN.html

web/entries/Abortable_Linearizable_Modules.html

web/entries/Abs_Int_ITP2012.html

web/entries/Abstract-Hoare-Logics.html

web/entries/Abstract-Rewriting.html

web/entries/Abstract_Completeness.html

web/entries/Abstract_Soundness.html

web/entries/Ackermanns_not_PR.html

web/entries/Actuarial_Mathematics.html

web/entries/Adaptive_State_Counting.html

web/entries/Affine_Arithmetic.html

web/entries/Aggregation_Algebras.html

web/entries/Akra_Bazzi.html

web/entries/Algebraic_Numbers.html

web/entries/Algebraic_VCs.html

web/entries/Allen_Calculus.html

web/entries/Amicable_Numbers.html

web/entries/Amortized_Complexity.html

web/entries/AnselmGod.html

web/entries/Applicative_Lifting.html

web/entries/Approximation_Algorithms.html

web/entries/Architectural_Design_Patterns.html

web/entries/Aristotles_Assertoric_Syllogistic.html

web/entries/Arith_Prog_Rel_Primes.html

web/entries/ArrowImpossibilityGS.html

web/entries/Attack_Trees.html

web/entries/Auto2_HOL.html

web/entries/Auto2_Imperative_HOL.html

web/entries/AutoFocus-Stream.html

web/entries/Automated_Stateful_Protocol_Verification.html

web/entries/Automatic_Refinement.html

web/entries/AxiomaticCategoryTheory.html

web/entries/BDD.html

web/entries/BD_Security_Compositional.html

web/entries/BNF_CC.html

web/entries/BNF_Operations.html

web/entries/BTree.html

web/entries/Banach_Steinhaus.html

web/entries/Belief_Revision.html

web/entries/Bell_Numbers_Spivey.html

web/entries/BenOr_Kozen_Reif.html

web/entries/Berlekamp_Zassenhaus.html

web/entries/Bernoulli.html

web/entries/Bertrands_Postulate.html

web/entries/Bicategory.html

web/entries/BinarySearchTree.html

web/entries/Binding_Syntax_Theory.html

web/entries/Binomial-Heaps.html

web/entries/Binomial-Queues.html

web/entries/BirdKMP.html

web/entries/Blue_Eyes.html

web/entries/Bondy.html

web/entries/Boolean_Expression_Checkers.html

web/entries/Boolos_Curious_Inference.html

web/entries/Bounded_Deducibility_Security.html

web/entries/Buchi_Complementation.html

web/entries/Budan_Fourier.html

web/entries/Buffons_Needle.html

web/entries/Buildings.html

web/entries/BytecodeLogicJmlTypes.html

web/entries/C2KA_DistributedSystems.html

web/entries/CAVA_Automata.html

web/entries/CAVA_LTL_Modelchecker.html

web/entries/CCS.html

web/entries/CISC-Kernel.html

web/entries/CRDT.html

web/entries/CSP_RefTK.html

web/entries/CYK.html

web/entries/CZH_Elementary_Categories.html

web/entries/CZH_Foundations.html

web/entries/CZH_Universal_Constructions.html

web/entries/CakeML.html

web/entries/CakeML_Codegen.html

web/entries/Call_Arity.html

web/entries/Card_Equiv_Relations.html

web/entries/Card_Multisets.html

web/entries/Card_Number_Partitions.html

web/entries/Card_Partitions.html

web/entries/Cartan_FP.html

web/entries/Case_Labeling.html

web/entries/Catalan_Numbers.html

web/entries/Category.html

web/entries/Category2.html

web/entries/Category3.html

web/entries/Cauchy.html

web/entries/Cayley_Hamilton.html

web/entries/Certification_Monads.html

web/entries/Chandy_Lamport.html

web/entries/Chord_Segments.html

web/entries/Circus.html

web/entries/Clean.html

web/entries/Clique_and_Monotone_Circuits.html

web/entries/ClockSynchInst.html

web/entries/Closest_Pair_Points.html

web/entries/CoCon.html

web/entries/CoSMeDis.html

web/entries/CoSMed.html

web/entries/CofGroups.html

web/entries/Coinductive.html

web/entries/Coinductive_Languages.html

web/entries/Collections.html

web/entries/Combinable_Wands.html

web/entries/Combinatorics_Words.html

web/entries/Combinatorics_Words_Graph_Lemma.html

web/entries/Combinatorics_Words_Lyndon.html

web/entries/Comparison_Sort_Lower_Bound.html

web/entries/Compiling-Exceptions-Correctly.html

web/entries/Complete_Non_Orders.html

web/entries/Completeness.html

web/entries/Complex_Bounded_Operators.html

web/entries/Complex_Geometry.html

web/entries/Complx.html

web/entries/ComponentDependencies.html

web/entries/ConcurrentGC.html

web/entries/ConcurrentIMP.html

web/entries/Concurrent_Ref_Alg.html

web/entries/Concurrent_Revisions.html

web/entries/Conditional_Simplification.html

web/entries/Conditional_Transfer_Rule.html

web/entries/Consensus_Refined.html

web/entries/Constructive_Cryptography.html

web/entries/Constructive_Cryptography_CM.html

web/entries/Constructor_Funs.html

web/entries/Containers.html

web/entries/CoreC++.html

web/entries/Core_DOM.html

web/entries/Core_SC_DOM.html

web/entries/Correctness_Algebras.html

web/entries/Cotangent_PFD_Formula.html

web/entries/Count_Complex_Roots.html

web/entries/CryptHOL.html

web/entries/CryptoBasedCompositionalProperties.html

web/entries/Cubic_Quartic_Equations.html

web/entries/DFS_Framework.html

web/entries/DOM_Components.html

web/entries/DPRM_Theorem.html

web/entries/DPT-SAT-Solver.html

web/entries/DataRefinementIBP.html

web/entries/Datatype_Order_Generator.html

web/entries/Decl_Sem_Fun_PL.html

web/entries/Decreasing-Diagrams-II.html

web/entries/Decreasing-Diagrams.html

web/entries/Dedekind_Real.html

web/entries/Deep_Learning.html

web/entries/Delta_System_Lemma.html

web/entries/Density_Compiler.html

web/entries/Dependent_SIFUM_Refinement.html

web/entries/Dependent_SIFUM_Type_Systems.html

web/entries/Depth-First-Search.html

web/entries/Derangements.html

web/entries/Deriving.html

web/entries/Descartes_Sign_Rule.html

web/entries/Design_Theory.html

web/entries/Dict_Construction.html

web/entries/Differential_Dynamic_Logic.html

web/entries/Differential_Game_Logic.html

web/entries/Digit_Expansions.html

web/entries/Dijkstra_Shortest_Path.html

web/entries/Diophantine_Eqns_Lin_Hom.html

web/entries/Dirichlet_L.html

web/entries/Dirichlet_Series.html

web/entries/DiscretePricing.html

web/entries/Discrete_Summation.html

web/entries/DiskPaxos.html

web/entries/Dominance_CHK.html

web/entries/DynamicArchitectures.html

web/entries/Dynamic_Tables.html

web/entries/E_Transcendental.html

web/entries/Echelon_Form.html

web/entries/EdmondsKarp_Maxflow.html

web/entries/Efficient-Mergesort.html

web/entries/Elliptic_Curves_Group_Law.html

web/entries/Encodability_Process_Calculi.html

web/entries/Epistemic_Logic.html

web/entries/Equivalence_Relation_Enumeration.html

web/entries/Ergodic_Theory.html

web/entries/Error_Function.html

web/entries/Euler_MacLaurin.html

web/entries/Euler_Partition.html

web/entries/Eval_FO.html

web/entries/Extended_Finite_State_Machine_Inference.html

web/entries/Extended_Finite_State_Machines.html

web/entries/FFT.html

web/entries/FLP.html

web/entries/FOL-Fitting.html

web/entries/FOL_Axiomatic.html

web/entries/FOL_Harrison.html

web/entries/FOL_Seq_Calc1.html

web/entries/FOL_Seq_Calc2.html

web/entries/FOL_Seq_Calc3.html

web/entries/FO_Theory_Rewriting.html

web/entries/Factor_Algebraic_Polynomial.html

web/entries/Factored_Transition_System_Bounding.html

web/entries/Falling_Factorial_Sum.html

web/entries/Farkas.html

web/entries/FeatherweightJava.html

web/entries/Featherweight_OCL.html

web/entries/Fermat3_4.html

web/entries/FileRefinement.html

web/entries/FinFun.html

web/entries/Finger-Trees.html

web/entries/Finite-Map-Extras.html

web/entries/Finite_Automata_HF.html

web/entries/Finite_Fields.html

web/entries/Finitely_Generated_Abelian_Groups.html

web/entries/First_Order_Terms.html

web/entries/First_Welfare_Theorem.html

web/entries/Fishburn_Impossibility.html

web/entries/Fisher_Yates.html

web/entries/Fishers_Inequality.html

web/entries/Flow_Networks.html

web/entries/Floyd_Warshall.html

web/entries/Flyspeck-Tame.html

web/entries/FocusStreamsCaseStudies.html

web/entries/Forcing.html

web/entries/Formal_Puiseux_Series.html

web/entries/Formal_SSA.html

web/entries/Formula_Derivatives.html

web/entries/Foundation_of_geometry.html

web/entries/Fourier.html

web/entries/Free-Boolean-Algebra.html

web/entries/Free-Groups.html

web/entries/Frequency_Moments.html

web/entries/Fresh_Identifiers.html

web/entries/FunWithFunctions.html

web/entries/FunWithTilings.html

web/entries/Functional-Automata.html

web/entries/Functional_Ordered_Resolution_Prover.html

web/entries/Furstenberg_Topology.html

web/entries/GPU_Kernel_PL.html

web/entries/Gabow_SCC.html

web/entries/GaleStewart_Games.html

web/entries/Gale_Shapley.html

web/entries/Game_Based_Crypto.html

web/entries/Gauss-Jordan-Elim-Fun.html

web/entries/Gauss_Jordan.html

web/entries/Gauss_Sums.html

web/entries/Gaussian_Integers.html

web/entries/GenClock.html

web/entries/General-Triangle.html

web/entries/Generalized_Counting_Sort.html

web/entries/Generic_Deriving.html

web/entries/Generic_Join.html

web/entries/GewirthPGCProof.html

web/entries/Girth_Chromatic.html

web/entries/GoedelGod.html

web/entries/Goedel_HFSet_Semantic.html

web/entries/Goedel_HFSet_Semanticless.html

web/entries/Goedel_Incompleteness.html

web/entries/Goodstein_Lambda.html

web/entries/GraphMarkingIBP.html

web/entries/Graph_Saturation.html

web/entries/Graph_Theory.html

web/entries/Green.html

web/entries/Groebner_Bases.html

web/entries/Groebner_Macaulay.html

web/entries/Gromov_Hyperbolicity.html

web/entries/Grothendieck_Schemes.html

web/entries/Group-Ring-Module.html

web/entries/HOL-CSP.html

web/entries/HOLCF-Prelude.html

web/entries/HRB-Slicing.html

web/entries/Hahn_Jordan_Decomposition.html

web/entries/Heard_Of.html

web/entries/Hello_World.html

web/entries/HereditarilyFinite.html

web/entries/Hermite.html

web/entries/Hermite_Lindemann.html

web/entries/Hidden_Markov_Models.html

web/entries/Higher_Order_Terms.html

web/entries/Hoare_Time.html

web/entries/Hood_Melville_Queue.html

web/entries/HotelKeyCards.html

web/entries/Huffman.html

web/entries/Hybrid_Logic.html

web/entries/Hybrid_Multi_Lane_Spatial_Logic.html

web/entries/Hybrid_Systems_VCs.html

web/entries/HyperCTL.html

web/entries/Hyperdual.html

web/entries/IEEE_Floating_Point.html

web/entries/IFC_Tracking.html

web/entries/IMAP-CRDT.html

web/entries/IMO2019.html

web/entries/IMP2.html

web/entries/IMP2_Binary_Heap.html

web/entries/IMP_Compiler.html

web/entries/IP_Addresses.html

web/entries/Imperative_Insertion_Sort.html

web/entries/Impossible_Geometry.html

web/entries/Incompleteness.html

web/entries/Incredible_Proof_Machine.html

web/entries/Independence_CH.html

web/entries/Inductive_Confidentiality.html

web/entries/Inductive_Inference.html

web/entries/InfPathElimination.html

web/entries/InformationFlowSlicing.html

web/entries/InformationFlowSlicing_Inter.html

web/entries/Integration.html

web/entries/Interpolation_Polynomials_HOL_Algebra.html

web/entries/Interpreter_Optimizations.html

web/entries/Interval_Arithmetic_Word32.html

web/entries/Intro_Dest_Elim.html

web/entries/Iptables_Semantics.html

web/entries/Irrational_Series_Erdos_Straus.html

web/entries/Irrationality_J_Hancl.html

web/entries/Irrationals_From_THEBOOK.html

web/entries/IsaGeoCoq.html

web/entries/IsaNet.html

web/entries/Isabelle_C.html

web/entries/Isabelle_Marries_Dirac.html

web/entries/Isabelle_Meta_Model.html

web/entries/Jacobson_Basic_Algebra.html

web/entries/Jinja.html

web/entries/JinjaDCI.html

web/entries/JinjaThreads.html

web/entries/JiveDataStoreModel.html

web/entries/Jordan_Hoelder.html

web/entries/Jordan_Normal_Form.html

web/entries/KAD.html

web/entries/KAT_and_DRA.html

web/entries/KBPs.html

web/entries/KD_Tree.html

web/entries/Key_Agreement_Strong_Adversaries.html

web/entries/Kleene_Algebra.html

web/entries/Knights_Tour.html

web/entries/Knot_Theory.html

web/entries/Knuth_Bendix_Order.html

web/entries/Knuth_Morris_Pratt.html

web/entries/Koenigsberg_Friendship.html

web/entries/Kruskal.html

web/entries/Kuratowski_Closure_Complement.html

web/entries/LLL_Basis_Reduction.html

web/entries/LLL_Factorization.html

web/entries/LOFT.html

web/entries/LP_Duality.html

web/entries/LTL.html

web/entries/LTL_Master_Theorem.html

web/entries/LTL_Normal_Form.html

web/entries/LTL_to_DRA.html

web/entries/LTL_to_GBA.html

web/entries/Lam-ml-Normalization.html

web/entries/LambdaAuth.html

web/entries/LambdaMu.html

web/entries/Lambda_Free_EPO.html

web/entries/Lambda_Free_KBOs.html

web/entries/Lambda_Free_RPOs.html

web/entries/Lambert_W.html

web/entries/Landau_Symbols.html

web/entries/Laplace_Transform.html

web/entries/Latin_Square.html

web/entries/LatticeProperties.html

web/entries/Launchbury.html

web/entries/Laws_of_Large_Numbers.html

web/entries/Lazy-Lists-II.html

web/entries/Lazy_Case.html

web/entries/Lehmer.html

web/entries/Lifting_Definition_Option.html

web/entries/Lifting_the_Exponent.html

web/entries/LightweightJava.html

web/entries/LinearQuantifierElim.html

web/entries/Linear_Inequalities.html

web/entries/Linear_Programming.html

web/entries/Linear_Recurrences.html

web/entries/Liouville_Numbers.html

web/entries/List-Index.html

web/entries/List-Infinite.html

web/entries/List_Interleaving.html

web/entries/List_Inversions.html

web/entries/List_Update.html

web/entries/LocalLexing.html

web/entries/Localization_Ring.html

web/entries/Locally-Nameless-Sigma.html

web/entries/Logging_Independent_Anonymity.html

web/entries/Lowe_Ontological_Argument.html

web/entries/Lower_Semicontinuous.html

web/entries/Lp.html

web/entries/Lucas_Theorem.html

web/entries/MDP-Algorithms.html

web/entries/MDP-Rewards.html

web/entries/MFMC_Countable.html

web/entries/MFODL_Monitor_Optimized.html

web/entries/MFOTL_Monitor.html

web/entries/MSO_Regex_Equivalence.html

web/entries/Markov_Models.html

web/entries/Marriage.html

web/entries/Mason_Stothers.html

web/entries/Matrices_for_ODEs.html

web/entries/Matrix.html

web/entries/Matrix_Tensor.html

web/entries/Matroids.html

web/entries/Max-Card-Matching.html

web/entries/Median_Method.html

web/entries/Median_Of_Medians_Selection.html

web/entries/Menger.html

web/entries/Mereology.html

web/entries/Mersenne_Primes.html

web/entries/Metalogic_ProofChecker.html

web/entries/MiniML.html

web/entries/MiniSail.html

web/entries/Minimal_SSA.html

web/entries/Minkowskis_Theorem.html

web/entries/Minsky_Machines.html

web/entries/Modal_Logics_for_NTS.html

web/entries/Modular_Assembly_Kit_Security.html

web/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html

web/entries/Monad_Memo_DP.html

web/entries/Monad_Normalisation.html

web/entries/MonoBoolTranAlgebra.html

web/entries/MonoidalCategory.html

web/entries/Monomorphic_Monad.html

web/entries/MuchAdoAboutTwo.html

web/entries/Multi_Party_Computation.html

web/entries/Multirelations.html

web/entries/Multiset_Ordering_NPC.html

web/entries/Myhill-Nerode.html

web/entries/Name_Carrying_Type_Inference.html

web/entries/Nash_Williams.html

web/entries/Nat-Interval-Logic.html

web/entries/Native_Word.html

web/entries/Nested_Multisets_Ordinals.html

web/entries/Network_Security_Policy_Verification.html

web/entries/Neumann_Morgenstern_Utility.html

web/entries/No_FTL_observers.html

web/entries/Nominal2.html

web/entries/Noninterference_CSP.html

web/entries/Noninterference_Concurrent_Composition.html

web/entries/Noninterference_Generic_Unwinding.html

web/entries/Noninterference_Inductive_Unwinding.html

web/entries/Noninterference_Ipurge_Unwinding.html

web/entries/Noninterference_Sequential_Composition.html

web/entries/NormByEval.html

web/entries/Nullstellensatz.html

web/entries/Octonions.html

web/entries/OpSets.html

web/entries/Open_Induction.html

web/entries/Optics.html

web/entries/Optimal_BST.html

web/entries/Orbit_Stabiliser.html

web/entries/Order_Lattice_Props.html

web/entries/Ordered_Resolution_Prover.html

web/entries/Ordinal.html

web/entries/Ordinal_Partitions.html

web/entries/Ordinals_and_Cardinals.html

web/entries/Ordinary_Differential_Equations.html

web/entries/PAC_Checker.html

web/entries/PAL.html

web/entries/PCF.html

web/entries/PLM.html

web/entries/POPLmark-deBruijn.html

web/entries/PSemigroupsConvolution.html

web/entries/Package_logic.html

web/entries/Padic_Ints.html

web/entries/Pairing_Heap.html

web/entries/Paraconsistency.html

web/entries/Parity_Game.html

web/entries/Partial_Function_MR.html

web/entries/Partial_Order_Reduction.html

web/entries/Password_Authentication_Protocol.html

web/entries/Pell.html

web/entries/Perfect-Number-Thm.html

web/entries/Perron_Frobenius.html

web/entries/Physical_Quantities.html

web/entries/Pi_Calculus.html

web/entries/Pi_Transcendental.html

web/entries/Planarity_Certificates.html

web/entries/Pluennecke_Ruzsa_Inequality.html

web/entries/Poincare_Bendixson.html

web/entries/Poincare_Disc.html

web/entries/Polynomial_Factorization.html

web/entries/Polynomial_Interpolation.html

web/entries/Polynomials.html

web/entries/Pop_Refinement.html

web/entries/Posix-Lexing.html

web/entries/Possibilistic_Noninterference.html

web/entries/Power_Sum_Polynomials.html

web/entries/Pratt_Certificate.html

web/entries/Prefix_Free_Code_Combinators.html

web/entries/Presburger-Automata.html

web/entries/Prim_Dijkstra_Simple.html

web/entries/Prime_Distribution_Elementary.html

web/entries/Prime_Harmonic_Series.html

web/entries/Prime_Number_Theorem.html

web/entries/Priority_Queue_Braun.html

web/entries/Priority_Search_Trees.html

web/entries/Probabilistic_Noninterference.html

web/entries/Probabilistic_Prime_Tests.html

web/entries/Probabilistic_System_Zoo.html

web/entries/Probabilistic_Timed_Automata.html

web/entries/Probabilistic_While.html

web/entries/Program-Conflict-Analysis.html

web/entries/Progress_Tracking.html

web/entries/Projective_Geometry.html

web/entries/Projective_Measurements.html

web/entries/Promela.html

web/entries/Proof_Strategy_Language.html

web/entries/PropResPI.html

web/entries/Propositional_Proof_Systems.html

web/entries/Prpu_Maxflow.html

web/entries/PseudoHoops.html

web/entries/Psi_Calculi.html

web/entries/Ptolemys_Theorem.html

web/entries/Public_Announcement_Logic.html

web/entries/QHLProver.html

web/entries/QR_Decomposition.html

web/entries/Quantales.html

web/entries/Quasi_Borel_Spaces.html

web/entries/Quaternions.html

web/entries/Quick_Sort_Cost.html

web/entries/RIPEMD-160-SPARK.html

web/entries/ROBDD.html

web/entries/RSAPSS.html

web/entries/Ramsey-Infinite.html

web/entries/Random_BSTs.html

web/entries/Random_Graph_Subgraph_Threshold.html

web/entries/Randomised_BSTs.html

web/entries/Randomised_Social_Choice.html

web/entries/Rank_Nullity_Theorem.html

web/entries/Real_Impl.html

web/entries/Real_Power.html

web/entries/Real_Time_Deque.html

web/entries/Recursion-Addition.html

web/entries/Recursion-Theory-I.html

web/entries/Refine_Imperative_HOL.html

web/entries/Refine_Monadic.html

web/entries/RefinementReactive.html

web/entries/Regex_Equivalence.html

web/entries/Registers.html

web/entries/Regression_Test_Selection.html

web/entries/Regular-Sets.html

web/entries/Regular_Algebras.html

web/entries/Regular_Tree_Relations.html

web/entries/Relation_Algebra.html

web/entries/Relational-Incorrectness-Logic.html

web/entries/Relational_Disjoint_Set_Forests.html

web/entries/Relational_Forests.html

web/entries/Relational_Method.html

web/entries/Relational_Minimum_Spanning_Trees.html

web/entries/Relational_Paths.html

web/entries/Rep_Fin_Groups.html

web/entries/ResiduatedTransitionSystem.html

web/entries/Residuated_Lattices.html

web/entries/Resolution_FOL.html

web/entries/Rewrite_Properties_Reduction.html

web/entries/Rewriting_Z.html

web/entries/Ribbon_Proofs.html

web/entries/Robbins-Conjecture.html

web/entries/Robinson_Arithmetic.html

web/entries/Root_Balanced_Tree.html

web/entries/Roth_Arithmetic_Progressions.html

web/entries/Routing.html

web/entries/Roy_Floyd_Warshall.html

web/entries/SATSolverVerification.html

web/entries/SC_DOM_Components.html

web/entries/SDS_Impossibility.html

web/entries/SIFPL.html

web/entries/SIFUM_Type_Systems.html

web/entries/SPARCv8.html

web/entries/Safe_Distance.html

web/entries/Safe_OCL.html

web/entries/Saturation_Framework.html

web/entries/Saturation_Framework_Extensions.html

web/entries/Schutz_Spacetime.html

web/entries/Secondary_Sylow.html

web/entries/Security_Protocol_Refinement.html

web/entries/Selection_Heap_Sort.html

web/entries/SenSocialChoice.html

web/entries/Separata.html

web/entries/Separation_Algebra.html

web/entries/Separation_Logic_Imperative_HOL.html

web/entries/SequentInvertibility.html

web/entries/Shadow_DOM.html

web/entries/Shadow_SC_DOM.html

web/entries/Shivers-CFA.html

web/entries/ShortestPath.html

web/entries/Show.html

web/entries/Sigma_Commit_Crypto.html

web/entries/Signature_Groebner.html

web/entries/Simpl.html

web/entries/Simple_Firewall.html

web/entries/Simplex.html

web/entries/Simplicial_complexes_and_boolean_functions.html

web/entries/SimplifiedOntologicalArgument.html

web/entries/Skew_Heap.html

web/entries/Skip_Lists.html

web/entries/Slicing.html

web/entries/Sliding_Window_Algorithm.html

web/entries/Smith_Normal_Form.html

web/entries/Smooth_Manifolds.html

web/entries/Sophomores_Dream.html

web/entries/Sort_Encodings.html

web/entries/Source_Coding_Theorem.html

web/entries/SpecCheck.html

web/entries/Special_Function_Bounds.html

web/entries/Splay_Tree.html

web/entries/Sqrt_Babylonian.html

web/entries/Stable_Matching.html

web/entries/Statecharts.html

web/entries/Stateful_Protocol_Composition_and_Typing.html

web/entries/Stellar_Quorums.html

web/entries/Stern_Brocot.html

web/entries/Stewart_Apollonius.html

web/entries/Stirling_Formula.html

web/entries/Stochastic_Matrices.html

web/entries/Stone_Algebras.html

web/entries/Stone_Kleene_Relation_Algebras.html

web/entries/Stone_Relation_Algebras.html

web/entries/Store_Buffer_Reduction.html

web/entries/Stream-Fusion.html

web/entries/Stream_Fusion_Code.html

web/entries/Strong_Security.html

web/entries/Sturm_Sequences.html

web/entries/Sturm_Tarski.html

web/entries/Stuttering_Equivalence.html

web/entries/Subresultants.html

web/entries/Subset_Boolean_Algebras.html

web/entries/SumSquares.html

web/entries/Sunflowers.html

web/entries/SuperCalc.html

web/entries/Surprise_Paradox.html

web/entries/Symmetric_Polynomials.html

web/entries/Syntax_Independent_Logic.html

web/entries/Szemeredi_Regularity.html

web/entries/Szpilrajn.html

web/entries/TESL_Language.html

web/entries/TLA.html

web/entries/Tail_Recursive_Functions.html

web/entries/Tarskis_Geometry.html

web/entries/Taylor_Models.html

web/entries/Three_Circles.html

web/entries/Timed_Automata.html

web/entries/Topological_Semantics.html

web/entries/Topology.html

web/entries/TortoiseHare.html

web/entries/Transcendence_Series_Hancl_Rucki.html

web/entries/Transformer_Semantics.html

web/entries/Transition_Systems_and_Automata.html

web/entries/Transitive-Closure-II.html

web/entries/Transitive-Closure.html

web/entries/Transitive_Models.html

web/entries/Treaps.html

web/entries/Tree-Automata.html

web/entries/Tree_Decomposition.html

web/entries/Triangle.html

web/entries/Trie.html

web/entries/Twelvefold_Way.html

web/entries/Tycon.html

web/entries/Types_Tableaus_and_Goedels_God.html

web/entries/Types_To_Sets_Extension.html

web/entries/UPF.html

web/entries/UPF_Firewall.html

web/entries/UTP.html

web/entries/Universal_Hash_Families.html

web/entries/Universal_Turing_Machine.html

web/entries/UpDown_Scheme.html

web/entries/VYDRA_MDL.html

web/entries/Valuation.html

web/entries/Van_Emde_Boas_Trees.html

web/entries/Van_der_Waerden.html

web/entries/VectorSpace.html

web/entries/VeriComp.html

web/entries/Verified-Prover.html

web/entries/Verified_SAT_Based_AI_Planning.html

web/entries/VerifyThis2018.html

web/entries/VerifyThis2019.html

web/entries/Vickrey_Clarke_Groves.html

web/entries/Virtual_Substitution.html

web/entries/VolpanoSmith.html

web/entries/WHATandWHERE_Security.html

web/entries/WOOT_Strong_Eventual_Consistency.html

web/entries/WebAssembly.html

web/entries/Weight_Balanced_Trees.html

web/entries/Weighted_Path_Order.html

web/entries/Well_Quasi_Orders.html

web/entries/Wetzels_Problem.html

web/entries/Winding_Number_Eval.html

web/entries/Word_Lib.html

web/entries/WorkerWrapper.html

web/entries/X86_Semantics.html

web/entries/XML.html

web/entries/Youngs_Inequality.html

web/entries/ZFC_in_HOL.html

web/entries/Zeta_3_Irrational.html

web/entries/Zeta_Function.html

web/entries/index.html

web/entries/index.xml

web/entries/pGCL.html

web/index.html

web/index.json

web/index.xml

web/sitemap.xml

web/statistics/index.html

web/theories/boolos_curious_inference/index.html

web/theories/index.xml

web/theories/word_lib/index.html

web/topics/index.html

web/topics/logic/philosophical-aspects/index.html

web/topics/logic/philosophical-aspects/index.xml