Diffusion afp-devel 1b6cf3461109

merge of AFP 2021-1
1b6cf3461109
Actions

Tags

None

Subscribers

None

Description

merge of AFP 2021-1

Details

Provenance

Rene Thiemann <rene.thiemann@uibk.ac.at>

Authored on

Parents

rAFPebe485ce088a: New AFP entry: Equivalence_Relation_Enumeration
rAFP1bf09a5c7053: Strong soundness.

Branches

Unknown

Tags

Unknown

Event Timeline

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP1b6cf3461109: merge of AFP 2021-1.Feb 7 2022, 10:29 AM

Merged Changes

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

1bf09a5c7053 Strong soundness.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
e58170bdc3c1 Strong soundness.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
65f692dc5bbe Fix LaTeX issue.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
2d18ab671110 Qualification required(?)
Author
nipkow
Browse Repository
No Builds
No Audits
f615acb4aac4 merged
Author
nipkow
Browse Repository
No Builds
No Audits
64393a5f8dc2 more variants of the algorithm
Author
nipkow
Browse Repository
No Builds
No Audits
ffd7c1f68029 Added funding acknowledgments.
Author
Dominique Unruh <unruh@ut.ee>
Browse Repository
No Builds
No Audits
febc0f010210 Strong completeness for PAL systems.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
8f595e5bd261 hugo site: updated site templates;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
b37dd66c6996 Cleanup.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
761895c0a8b8 Fewer parentheses around turnstile + remove unused lemmas.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
7d3ad94c215c Simplify proof of truth lemma.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
be7352e7c0e2 Notation for `imply` and fewer parenthesis around turnstiles.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
cf7d5176f108 Abstract results to shorten proofs.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
6174f4badbac Better notation.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
09a3e2523fd9 metadata migration: updated authors;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
bd32b1fd6406 merged
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d80eeff3bd7d hugo: added mobile view;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9be5074d44ca hugo: copy to proper path;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
c1393433f082 merged
Author
makarius
Browse Repository
No Builds
No Audits
6ef2e075a034 tuned whitespace;
Author
makarius
Browse Repository
No Builds
No Audits
6136280343a0 more symbols;
Author
makarius
Browse Repository
No Builds
No Audits
e5dd226cebfc profer bundle lattice_syntax;
Author
makarius
Browse Repository
No Builds
No Audits
8cb75b461233 prefer existing lattice_syntax and no_lattice_syntax, with proper 'no_notation'…
Author
makarius
Browse Repository
No Builds
No Audits
1326d2e54798 Add soundness and completeness for the PAL versions of systems K, T, KB, K4, S4…
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
d002a4bd210d avoid hardwired document output;
Author
makarius
Browse Repository
No Builds
No Audits
abbaf3d0dbb2 merged
Author
paulson
Browse Repository
No Builds
No Audits
516413c9bc28 deleting the overloading of div and mod, with its attendant ambiguities
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
a148c50ef51f replaced Erdős by Erd\H{o}s (fixed problem in LaTeX document generation)
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
81aae6b30ce5 Removal of a lemma (now in the libraries) and a few tweaks
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
cc5747ff291e Tuning.
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
6772d0f44fcd merged
Author
paulson
Browse Repository
No Builds
No Audits
58ab4f651da2 tweaks
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
e1da0b0d0794 merged
Author
paulson
Browse Repository
No Builds
No Audits
b34d91e2ee32 Fixed an inadequate description
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
d858bca8a11d tuned
Author
florian.haftmann
Browse Repository
No Builds
No Audits
20e68f30d833 mv to distribution
Author
nipkow
Browse Repository
No Builds
No Audits
1e6800ff5ef5 by now in distribution
Author
nipkow
Browse Repository
No Builds
No Audits
bcab7766727b merge from afp-2021-1
Author
kleing
Browse Repository
No Builds
No Audits
241da1cdeabf CS: possibility to disable backtracking; CZH: auxiliary results; ETTS: minor…
Author
user9716869 <user9716869@gmail.com>
Browse Repository
No Builds
No Audits
c55c666012a3 used wfP_imp_asymp from HOL
Author
desharna
Browse Repository
No Builds
No Audits
cae2c55e7bbb simplified proof some more
Author
desharna
Browse Repository
No Builds
No Audits
1d3873e125b1 simplified proof
Author
desharna
Browse Repository
No Builds
No Audits
66d4e5d44d29 Extended protocol model to support composition of more than two protocols…
Author
Achim D. Brucker <adbrucker@0x5f.org>
Browse Repository
No Builds
No Audits
3e741a914079 Tweaked some failing proofs
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
e2ae9549a7b0 adapted to new Sledgehammer.run_sledgehammer return type
Author
desharna
Browse Repository
No Builds
No Audits
61d6f3a035a8 Strengthened a lemma
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
92c2345bc9bd updated the definition of scheme
Author
Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
Browse Repository
No Builds
No Audits
28e95145c4ac merge from afp-2021-1
Author
kleing
Browse Repository
No Builds
No Audits
9df0012013a7 merge from afp-2021-1
Author
kleing
Browse Repository
No Builds
No Audits

Changes (167)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

metadata/

Actuarial_Mathematics

Preliminaries.thy

Equivalence_Relation_Enumeration

Equivalence_Relation_Enumeration.thy

Completeness.thy

Countermodel.thy

EPathHintikka.thy

ProverLemmas.thy

Sequent_Calculus_Verifier.thy

ProofExtractor.hs

ProverInstances.hs

SeCaVTranslator.hs

secav-prover.cabal

Interpolation_Polynomials_HOL_Algebra

Bounded_Degree_Polynomials.thy

Interpolation_Polynomial_Cardinalities.thy

Lagrange_Interpolation.thy

Irrationals_From_THEBOOK

Irrationals_From_THEBOOK.thy

Minimum_Maximum.thy

Move_To_Matrix.thy

Quasi_Borel_Spaces

Bayesian_Linear_Regression.thy

Binary_CoProduct_QuasiBorel.thy

Binary_Product_QuasiBorel.thy

CoProduct_QuasiBorel.thy

Exponent_QuasiBorel.thy

Measure_QuasiBorel_Adjunction.thy

Measure_as_QuasiBorel_Measure.thy

Monad_QuasiBorel.thy

Pair_QuasiBorel_Measure.thy

Probability_Space_QuasiBorel.thy

Product_QuasiBorel.thy

StandardBorel.thy

Youngs_Inequality

Abstract-Rewriting.html

Abstract_Completeness.html

Abstract_Soundness.html

Actuarial_Mathematics.html

Algebraic_Numbers.html

Berlekamp_Zassenhaus.html

Card_Equiv_Relations.html

Certification_Monads.html

Collections.html

Cubic_Quartic_Equations.html

Datatype_Order_Generator.html

Depth-First-Search.html

Equivalence_Relation_Enumeration.html

FOL_Seq_Calc1.html

FOL_Seq_Calc2.html

Factor_Algebraic_Polynomial.html

First_Order_Terms.html

Interpolation_Polynomials_HOL_Algebra.html

Irrationals_From_THEBOOK.html

Jordan_Normal_Form.html

Knuth_Bendix_Order.html

LLL_Basis_Reduction.html

LLL_Factorization.html

LP_Duality.html

Lifting_Definition_Option.html

Linear_Inequalities.html

Median_Method.html

Modular_arithmetic_LLL_and_HNF_algorithms.html

Partial_Function_MR.html

Perron_Frobenius.html

Polynomial_Factorization.html

Polynomial_Interpolation.html

Polynomials.html

Quasi_Borel_Spaces.html

Regular_Tree_Relations.html

Sqrt_Babylonian.html

Stirling_Formula.html

Stochastic_Matrices.html

Subresultants.html

Sunflowers.html

Transitive-Closure-II.html

Transitive-Closure.html

Weighted_Path_Order.html

Youngs_Inequality.html

statistics.html

rAFP1b6cf3461109

metadata/metadata

thys/Actuarial_Mathematics/Interest.thy

thys/Actuarial_Mathematics/Preliminaries.thy

thys/Actuarial_Mathematics/ROOT

thys/Actuarial_Mathematics/document/root.tex

thys/Equivalence_Relation_Enumeration/Equivalence_Relation_Enumeration.thy

thys/Equivalence_Relation_Enumeration/ROOT

thys/Equivalence_Relation_Enumeration/document/root.bib

thys/Equivalence_Relation_Enumeration/document/root.tex

thys/FOL_Seq_Calc2/.gitignore

thys/FOL_Seq_Calc2/.hlint.yaml

thys/FOL_Seq_Calc2/Completeness.thy

thys/FOL_Seq_Calc2/Countermodel.thy

thys/FOL_Seq_Calc2/EPathHintikka.thy

thys/FOL_Seq_Calc2/Export.thy

thys/FOL_Seq_Calc2/Hintikka.thy

thys/FOL_Seq_Calc2/LICENSE

thys/FOL_Seq_Calc2/Makefile

thys/FOL_Seq_Calc2/Prover.thy

thys/FOL_Seq_Calc2/ProverLemmas.thy

thys/FOL_Seq_Calc2/README.md

thys/FOL_Seq_Calc2/ROOT

thys/FOL_Seq_Calc2/Results.thy

thys/FOL_Seq_Calc2/SeCaV.thy

thys/FOL_Seq_Calc2/Sequent1.thy

thys/FOL_Seq_Calc2/Sequent_Calculus_Verifier.thy

thys/FOL_Seq_Calc2/Setup.hs

thys/FOL_Seq_Calc2/Soundness.thy

thys/FOL_Seq_Calc2/Usemantics.thy

thys/FOL_Seq_Calc2/document/root.tex

thys/FOL_Seq_Calc2/haskell/app/Main.hs

thys/FOL_Seq_Calc2/haskell/lib/ProofExtractor.hs

thys/FOL_Seq_Calc2/haskell/lib/ProverInstances.hs

thys/FOL_Seq_Calc2/haskell/lib/SeCaVTranslator.hs

thys/FOL_Seq_Calc2/haskell/lib/ShortAST.hs

thys/FOL_Seq_Calc2/haskell/lib/ShortLexer.hs

thys/FOL_Seq_Calc2/haskell/lib/ShortParser.hs

thys/FOL_Seq_Calc2/haskell/lib/Unshortener.hs

thys/FOL_Seq_Calc2/secav-prover.cabal

thys/FOL_Seq_Calc2/test/completeness/ROOT

thys/FOL_Seq_Calc2/test/completeness/Runner.hs

thys/FOL_Seq_Calc2/test/completeness/Tests.hs

thys/FOL_Seq_Calc2/test/soundness/Runner.hs

thys/FOL_Seq_Calc2/test/soundness/Tests.hs

thys/Interpolation_Polynomials_HOL_Algebra/Bounded_Degree_Polynomials.thy

thys/Interpolation_Polynomials_HOL_Algebra/Interpolation_Polynomial_Cardinalities.thy

thys/Interpolation_Polynomials_HOL_Algebra/Lagrange_Interpolation.thy

thys/Interpolation_Polynomials_HOL_Algebra/ROOT

thys/Interpolation_Polynomials_HOL_Algebra/document/root.bib

thys/Interpolation_Polynomials_HOL_Algebra/document/root.tex

thys/Irrationals_From_THEBOOK/Irrationals_From_THEBOOK.thy

thys/Irrationals_From_THEBOOK/ROOT

thys/Irrationals_From_THEBOOK/document/root.bib

thys/Irrationals_From_THEBOOK/document/root.tex

thys/LP_Duality/LP_Duality.thy

thys/LP_Duality/Minimum_Maximum.thy

thys/LP_Duality/Move_To_Matrix.thy

thys/LP_Duality/ROOT

thys/LP_Duality/document/root.bib

thys/LP_Duality/document/root.tex

thys/Median_Method/Median.thy

thys/Median_Method/ROOT

thys/Median_Method/document/root.bib

thys/Median_Method/document/root.tex

thys/Quasi_Borel_Spaces/Bayesian_Linear_Regression.thy

thys/Quasi_Borel_Spaces/Binary_CoProduct_QuasiBorel.thy

thys/Quasi_Borel_Spaces/Binary_Product_QuasiBorel.thy

thys/Quasi_Borel_Spaces/CoProduct_QuasiBorel.thy

thys/Quasi_Borel_Spaces/Exponent_QuasiBorel.thy

thys/Quasi_Borel_Spaces/Measure_QuasiBorel_Adjunction.thy

thys/Quasi_Borel_Spaces/Measure_as_QuasiBorel_Measure.thy

thys/Quasi_Borel_Spaces/Monad_QuasiBorel.thy

thys/Quasi_Borel_Spaces/Pair_QuasiBorel_Measure.thy

thys/Quasi_Borel_Spaces/Probability_Space_QuasiBorel.thy

thys/Quasi_Borel_Spaces/Product_QuasiBorel.thy

thys/Quasi_Borel_Spaces/QuasiBorel.thy

thys/Quasi_Borel_Spaces/ROOT

thys/Quasi_Borel_Spaces/StandardBorel.thy

thys/Quasi_Borel_Spaces/document/root.bib

thys/Quasi_Borel_Spaces/document/root.tex

thys/ROOTS

thys/Youngs_Inequality/ROOT

thys/Youngs_Inequality/Youngs.thy

thys/Youngs_Inequality/document/root.bib

thys/Youngs_Inequality/document/root.tex

web/entries/Abstract-Rewriting.html

web/entries/Abstract_Completeness.html

web/entries/Abstract_Soundness.html

web/entries/Actuarial_Mathematics.html

web/entries/Algebraic_Numbers.html

web/entries/Berlekamp_Zassenhaus.html

web/entries/Card_Equiv_Relations.html

web/entries/Certification_Monads.html

web/entries/Collections.html

web/entries/Cubic_Quartic_Equations.html

web/entries/Datatype_Order_Generator.html

web/entries/Depth-First-Search.html

web/entries/Deriving.html

web/entries/Equivalence_Relation_Enumeration.html

web/entries/FOL_Seq_Calc1.html

web/entries/FOL_Seq_Calc2.html

web/entries/Factor_Algebraic_Polynomial.html

web/entries/Farkas.html

web/entries/First_Order_Terms.html

web/entries/Interpolation_Polynomials_HOL_Algebra.html

web/entries/Irrationals_From_THEBOOK.html

web/entries/Jordan_Normal_Form.html

web/entries/Knuth_Bendix_Order.html

web/entries/LLL_Basis_Reduction.html

web/entries/LLL_Factorization.html

web/entries/LP_Duality.html

web/entries/Lifting_Definition_Option.html

web/entries/Linear_Inequalities.html

web/entries/Matrix.html

web/entries/Median_Method.html

web/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html

web/entries/Partial_Function_MR.html

web/entries/Perron_Frobenius.html

web/entries/Polynomial_Factorization.html

web/entries/Polynomial_Interpolation.html

web/entries/Polynomials.html

web/entries/Quasi_Borel_Spaces.html

web/entries/Real_Impl.html

web/entries/Regular_Tree_Relations.html

web/entries/Show.html

web/entries/Simplex.html

web/entries/Sqrt_Babylonian.html

web/entries/Stirling_Formula.html

web/entries/Stochastic_Matrices.html

web/entries/Subresultants.html

web/entries/Sunflowers.html

web/entries/Transitive-Closure-II.html

web/entries/Transitive-Closure.html

web/entries/Weighted_Path_Order.html

web/entries/XML.html

web/entries/Youngs_Inequality.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html