Thank you for this great metaphor that matches well with an anti-capitalist reading of the film.

Tabulka se nezobrazuje, protože odkazovaný obrázek neexistuje. URL obrázku: https://prod6vbzy22z.main.acsf.baywsf.com/sites/g/files/vrxlpx12926/files/2021-03/tabulka-spolehlivosti.jpg

A similar declaration is advised by Elsevier's Generative AI policies for journals:

During the preparation of this work the author(s) used [NAME TOOL / SERVICE] in order to [REASON]. After using this tool/service, the author(s) reviewed and edited the content as needed and take(s) full responsibility for the content of the publication.

Source: https://www.elsevier.com/about/policies-and-standards/generative-ai-policies-for-journals#4-frequently-asked-questions

https://www.elsevier.com/about/policies-and-standards/generative-ai-policies-for-journals

https://knihovna.cvut.cz/seminare-a-vyuka/jak-psat/jak-citovat?view=article&id=399:priklady-citaci-podle-csn-iso-690-4-vyd-2022&catid=12:seminare-a-vyuka#jak-citovat-ai---chatgpt

https://www.ckgame.net/

Daniela Pajtašová z Ústavu hematologie a krevní transfuze:

[P]o užití marihuany je třeba dodržet minimálně týden odstup, než půjdete darovat krev. Užití musí být výjimečné, pravidelné užívání se s dárcovstvím neslučuje.

[Užívání marihuany] více jak 1x za půl roku [je považováno za pravidelné].

[Krev od lidí, kteří užívají marihuanu pravidelně, není žádoucí] především [proto, že] je to známka dalšího možného rizikového chování.

Darovat krev tedy mohu, pokud jsem v posledním půlroce užil marihuanu maximálně jednou a od tohoto užití uplynul nejméně týden. Častější užívání marihuany je považováno za rizikové, protože značí další možné rizikové chování.

Daniela Pajtašová z Ústavu hematologie a krevní transfuze:

[P]o užití marihuany je třeba dodržet minimálně týden odstup, než půjdete darovat krev. Užití musí být výjimečné, pravidelné užívání se s dárcovstvím neslučuje.

[Užívání marihuany] více jak 1x za půl roku [je považováno za pravidelné].

[Krev od lidí, kteří užívají marihuanu pravidelně, není žádoucí] především [proto, že] je to známka dalšího možného rizikového chování.

Darovat krev tedy mohu, pokud jsem v posledním půlroce užil marihuanu maximálně jednou a od tohoto užití uplynul nejméně týden. Častější užívání marihuany je považováno za rizikové, protože značí další možné rizikové chování.

Training example: - Input: - Initial sensor readings - Sequence of actions - Output: - Final sensor readings - Augmented: Latent knowledge

We train jointly the sensor prediction task and a latent representation task.

What does this mean?

I think it should actually maximize my expected contribution, rather than "allow the biggest contribution".

1. Global cooperation incentives: Find incentives that motivate countries and MNCs to cooperate and act pro-socially.
2. Identify and promote efficient structures of cooperation on various levels (international, national, township, family etc.)
3. How to alleviate the suffering of the poorest

Potential future people who will never be born will never suffer. So even if I would like to prevent suffering of 100 future people, I might still not want to prevent a catastrophe.

See antinatalist arguments by Benatar.

The link is broken.

Our career quiz is no longer available.

Source: https://80000hours.org/career-quiz/

Guessing uniformly randomly would yield expected score of 10/3, which is worse than my score of 4.

privilege guilt

Why and how does this career guide target rich people, or people living in the Global North?

more good in terms of wellbeing

Income comparators: - https://www.givingwhatwecan.org/how-rich-am-i?income=68000&countryCode=USA&numAdults=1&numChildren=0 - https://wid.world/income-comparator/

An individual that makes $68,000 per year in the USA: - Income Comparator: 80th percentile (the same as a person earning 830 000 Kč per year in the Czech Republic) - How Rich Am I?: 99th percentile, 20.1 times the global median (the same as a person earning 1,025,000 Kč per year in the Czech Republic)

1. Humans have a very general ability to solve problems and achieve goals across diverse domains.
2. AI systems could become much more intelligent than humans.
3. If we create highly intelligent AI systems, their decisions will shape the future.
4. Highly intelligent AI systems won’t be beneficial by default.

The general mistrust of unknown agents may be grounded in a lesson from evolution: if a situation can be exploited, some agent likely will exploit it.

Does the disparate modules hypothesis claim that humans are not "much more cognitively versatile and adaptable than chimpanzees"?

Perhaps humans do have a collection of disparate modules and these modules are more general than looking at evolution would let us expect, but not completely general. Reducing the hypothesis to a qualitative one gives rise to a potentially false dilemma.

Alternative: Future ML Systems Will Be Qualitatively Different

Sounds like GOFAI (symbolic AI, automated deductive reasoning).

Failure to optimize the reward may be a competence issue rather than an alignment issue.

The reason is that no such situation appeared in the training data. The training data underrepresents such situations.

Ensure that the training data distribution matches the deployment data distribution.

Ensure that the loss (and the training data it depends on) corresponds to the intent.

or, more precisely, the intent behind the system prompts.

• Alignment
• Moral philosophy
• Competence
• Governance
• Resilience
• Security

V balení černé varianty najdete 3 silikonové potahy s různě velkými špunty.

3 velikosti silikonových nástavců

Zdroj: https://www.intezze.com/cz/dream-cerne

However, how large portion of this potential productivity growth will be realized? Is this 25 % of 2.6, or 4.4 trillion?

This article seems to cherry-pick signs of fast progress in AI.

This is an improvement over Steam Family Sharing.

This is an improvement over Steam Family Sharing.

https://www.mercusys.com/en/faq-773

Aktuální poplatek: max. 495 Kč/MWh

Code that reads and aggregates individual measurements: https://colab.research.google.com/drive/1ga25tsi2MMQ-zBdFLyO_ICqbB39IMrVD

$$\lnot p \land \lnot q$$

In logic, the monadic predicate calculus (also called monadic first-order logic) is the fragment of first-order logic in which all relation symbols in the signature are monadic (that is, they take only one argument), and there are no function symbols.

Source: https://en.wikipedia.org/wiki/Monadic_predicate_calculus

$$\forall i : x(i) \land y(i) \Leftrightarrow x(i)$$

What would suffice: $$\forall i : x(i) \Rightarrow y(i)$$

The LNCS LaTeX document class "llncs" suppresses Contents in the PDF metadata. See instructions for restoring the PDF table of contents here: https://comp.text.tex.narkive.com/r3o0LGOO/lncs-class-and-hyperref-package-missing-outline-as-pdf-bookmarks#post2

https://link.springer.com/book/10.1007/978-3-031-63498-7

https://link.springer.com/chapter/10.1007/978-3-031-63498-7_12

LCTRS

https://en.wikipedia.org/wiki/Kill_switch

AI systems trained by reinforcement learning are sometimes trained on maze-like tasks.

The riff resembles the riff in the verse "The only one I loved was you" in The Lover.

Na

přestože

According to this document, "[t]he last sentence of a [...] caption should end without a period".

Extended abstract and slides: https://github.com/filipbartek/wg5-vienna24/releases/tag/final

How do you generate the training data? How do you vary the encoding (direct vs. indirect)?

What if the trained NN misclassifies some training pairs (non-zero train loss) or test pairs (fails verification)?

How often does fitting the training data (traces) fail? - We train for 1k iterations.

How often does everything fail? - Reported in performance table.

How small are the NNs? - 1 hidden layer, 10 neurons

1. Train a NN
2. Verify that the NN is decreasing at every step and bounded from below (trivial) by encoding as a SMT problem

Is the size of the NN limited by the SMT verification runtime? - No, the formal verification takes very little time.

Do you or could you use various activation functions (nonlinear, log, exp, etc.) to train complex algebraic formulas? Would it make sense? - Somebody else has done something like this.

Can you make the NN stronger by making it deeper?

Alternative approach: Synthesize ranking function by CyGuS.

cvc5, instantiation, GNNs

If LLMs are good for humans, then ML for ATP is like training for several humans that speak very different languages (the solvers).

Why don't you instantiate all QEs in each round? - The classification threshold is very low (1x10-5), so almost all QEs are instantiated.

How many instances per QE do you generate? - 1 or 10.

Did you train on proofs generated by e-matching?

Frama-C

What is a perfect specification? One that exactly describes the behavior of the program as a black box.

Paper: https://arxiv.org/abs/2403.03997v1

With A* enumeration, what is the target of the search and how is the distance computed?

0930–1000 Alessandro Bruni: [formalization of probability theory in Coq] - MathComp-Analysis

• Why can we disregard the left hand side of the property?
• Do you always "fix" the NN using a particular sample and property?

Performance measures

• Precision (if the model is uncertain)
• Runtime or output length (algorithm selection)

How to generate data

• FWD Forwards - integrate
• BWD Backwards - differentiate
• IBP Per partes
• Risch
• Substitution

Representation of input formula

• LSTM
• TreeLSTM (recursive on AST)

Questions

• Is it a search? - No, just one selection per query.
• Why not just run all the algorithms (in parallel) and compare the results? If one call is always short ("we don't care about runtime"), we could run all. - No strong reason.
• Can you get training data (integration queries) from the users? - The test set contains queries from bug reports from the users.
• You could use Learning to rank to train an algorithm ranker (recommender) instead of a selector.
• You could run the standard simplification as a post-processing step.
• Multi-label classification: Why not use one NN with 12 outputs and cross-entropy loss to train a probability distribution (multi-class classification)? - No strong reason, it seems.
• How much slower is the TreeLSTM-based algorithm selector compared to the standard Maple's meta-algorithm? - The selector takes milliseconds to predict.
• How are the training examples weighted (balanced) across the generation methods? - Equal part for each method.

Actual start: 11:30

ML benchmark

• Input: Clauses
• Output: Next inference

no ML-friendly benchmark publicly available

Not even TSTP?

The ML task is specific to the prover. There cannot be a cross-prover benchmark.

Modular ATP

• Parser (TPTP etc.)
• Library of inference rules (micro-service architecture)

https://www.youtube.com/watch?v=FyeOPfg_6FE

Grand Old Party – Republikánská strana

In the figure "Years needed to buy a 75-square-meter flat", what is the source of the apartment prices?

Common search for a philosophical question

This passage is cited in From Science to Conscience as an introduction of regressive abstraction.

Domácnost má nárok na příspěvek, pokud je její měsíční příjem nižší než 20812 / 0.3 = 69373 Kč.

Admirable speaker!

At some point in the lecture, he asked the audience: "Raise your hand if you consider yourself to have a good background in supervised learning."

Zdroj?

Jak pracujeme s chronologií? Je chronologie důležitá?

Jak v sokratovském rozhovoru pracujeme s nedokonalostí paměti a domýšlením ("filling in the gaps")?

Hledám přiléhavější formulaci tohoto kritéria. Nápady: - Vypravěč má od popisovaných události dostatečný odstup

Co přesně tohle znamená?

Uvažováním nad hypotetickými situacemi se zabývají kontrafaktuály.

https://www.rferl.org/a/romania-sinking-village-geamana-waste-copper-mine/28436792.html

Jedná se o Rekreační a školící středisko Loutí?

Podobný postup je navržen ve cvičení 14. "Dialogue around a story" v knize "Free space: Field guide to conversations".

Leonard Nelson původně nechával účastníky, aby si zvolili téma sami na začátku rozhovoru.

Jak můžeme najít nebo poznat správnou míru pochybování (kritičnosti) a otevřenosti?

Podobného účinku by možná bylo lze dosáhnout simulací: lektor by na začátku požádal účastníky, aby sdíleli své zkušenosti se změnou názoru ("Kdy jste změnili názor?").

Opačným směrem jde kritické hodnocení toho, co slyšíme. K tomu by účastníci mohli sdílet zkušenosti, kdy něco, co slyšeli, zavrhli.

Jaký je rozdíl mezi rozhovorem a diskuzí?

https://cs.nyu.edu/~mohri/mlbook/

I have come up with two variants of Anti-Virus. Both of the variants challenge the players to plan their moves before executing them under a time pressure. Both of the variants are probably suitable for other games similar to Anti-Virus.

Look before you leap

Divide the process of solving a challenge into two phases, each of them timed:

1. Inspection ("look"): Inspect the challenge without touching any piece. Try to invent a plan of moving the pieces to solve the challenge.
2. Manipulation ("leap"): Physically move the pieces to solve the challenge.

Try to minimize the manipulation time at the expense of inspection time.

Multiplayer

Agree on a manipulation time limit, for example 1 minute. Choose and set up a challenge. Let all the players inspect the challenge. As soon as one of the players thinks they can solve the challenge within the manipulation time limit, they start a timer and manipulate the pieces. If they solve the challenge within the time limit, they win. If not, they return the pieces to their original positions and the remaining players can continue inspecting and attempting to solve the challenge.

2022-10-13 16:00

2022-10-12 11:00

Black-box optimization (maximization)

Explore first, exploit near the end: cf. simulated annealing, BO

Self-adjusting parameter selection

Adjust parameters during the run. The update depends on the success of previous iterations.

1-5th rule

• If mutation was successful, increase mutation probability (heat).
• If mutation was unsuccessful, decrease mutation probability (cool).

Dream: dynamic algorithm configuration

Select algorithm + HPs for next iteration from: - Previous experiments - Current optimization process state

ELA-based Algorithm Selection

Cf. SATZilla

https://tinyurl.com/2p9fm8z6

\(\pi\)BO is implemented in HyperMapper.

Links

• https://recommender-systems.com/
• https://github.com/ISG-Siegen/Auto-Surprise
• https://www.darwingoliath.com/

Goals of the lecture

• Have a secondary field of research besides AutoML
• Choose an interesting field of application for AutoML
• Look out of the box to improve AutoML

Types of recommendations

1. Rating prediction
2. Top-n ranking

AutoRecSys

Several rating prediction libraries exist. They focus on CASH (... algorithm selection ...) problem.

AutoDS

4 quadrants of AutoDS

• Data exploration
• Data engineering
• Model building - AutoML
• Exploitation

AutoML

• Architecture search
• HPO
• Meta-learning

Automatic Statistician

Data exploration

De Bie: Subjective interestingness (contrast with the data analyst's prior expectations)

Synth Research Camp

Data engineering

• Data wrangling

Inductive programming - FlashFill - FlashGPT3

Jesse Davis: time series to tabular data

Synth

Data engineering + AutoML + exploitation

Input: Partially filled set of tables

• Autocompete, autocorrect (?)
• Constraint satisfaction - e.g. employee shift rostering - "Populate each work shift with a nurse."
  • Constraint detection from data

Constraint learning

Few ML scientists learn constraints from data.

• Yields explainable models
• SMT constraint learning can be encoded as SMT problem (model search).

Autocompletion

MERCS - bidirectional regression and classification decision trees - cf. Bayesian networks (can they do regression?)

AD-MERCS - anomaly detection

Alternatives: - Psyche - probabilistic models - Probabilistic programming

AutoML for diverse tasks: cf. general game playing

automl.decathlon@gmail.com

Deadline for competitions: 2022-10-13 12:30

SMAC hands-on

2022-10-12 13:30

https://github.com/automl-edu/smac_fallschool22

For example Andrej Karpathy

• https://github.com/innixma/fall-automl-2022-autogluon
• https://github.com/gidler/autogluon-tutorials

https://www.vag-freiburg.de/tickets/einzel-und-tageskarten/2x4-fahrtenkarte

H2O only supports tabular datasets.

What makes the training nondeterministic: - Neural networks with more than 1 worker - Wallclock time limit

https://github.com/ledell/automl-fall-school-2022

How can Gaussian process be used with categorical variables?

I recommend this introduction to neural networks: https://www.3blue1brown.com/topics/neural-networks

Examples of art

• Helena Nikonole: Bird Language
• Interspecifics Collective: Recurrent Morphing Radio
  • Infinite music: cf. procedural music by Eno etc., generative.fm
• Dadabots: Relentless Doppleganger
• Hexorcismos: Transfiguracion (2020)

Glossary of machine learning

• Dataset
• Training
• Epoch
• Hyperparameters
  • Examples: Learning rate, number of epochs
• Weights/Checkpoints
• Inference/Prediction

Algorithms

• Autoencoder
• Variational autoencoder
• Generative adversarial network

Comments: - Doesn't the exponentiation of symbol weights make some symbols too heavy? - Use a simpler ML model - F: Example: Simple symbol features (arity, predicate/function, ...) - Train age-weight ratio too - Can you learn on larger sets of clauses than pairs?

github.com/data61/PSL

philosophers, logicians

Modules: - Parser - Proof state - Proof calculus - Clause encoder - Given clause selection guidance

Interface a prover should implement to be compatible: OpenAI Gym in Python

If the stochasticity of queue selection (age or weight) is useful, could selecting the next clause from the selected queue stochastically be similarly advantageous? We could use a geometric distribution to favor the clauses near the head of the queue.

Incremental learning: Solve as many problems in the problem set within an overall time budget (e.g. one week).

Uniform Budgeted Scheduler: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8 ...

Hindsight Experience Replay

Augmenting training data from failed proof searches:

We used to be data poor and now we are data rich.

Theorem: interesting, meaningful, valid in some theory

"interesting": David Hilbert: "One can measure the importance of a scientific work by the number of earlier publications rendered superfluous by it."

A new kind of mathematician: One who asks good questions to a perfect oracle (ATP)

We can piggy-back on existing interesting and meaningful theorems by searching for similar theorems - mutating them.

Original text in English: https://foreignpolicy.com/2022/05/27/russia-war-ukraine-genocide/

StarExec Miami machine specifications

8

How is this enforced? What benchmarking framework is used? Options: - runsolver - BenchExec

• Total Cores: 6
• Total Threads: 12

https://www.intel.com/content/www/us/en/products/sku/64589/intel-xeon-processor-e52667-15m-cache-2-90-ghz-8-00-gts-intel-qpi/specifications.html

when solver pipelines are used, a third argument will be present that contains the path to the additional output directory used by the previous stage.

Původní transparentní účet: https://www.csas.cz/cs/transparentni-ucty#/000000-4482788379

Citovaná zpráva: https://assets.publishing.service.gov.uk/government/uploads/system/uploads/attachment_data/file/1052353/Vaccine_surveillance_report_-_week_5.pdf

Death rates per 100k written in the report (Table 13): - Not vaccinated, 80+: 307.4 or 325.5 - Vaccinated with at least 3 doses, 80+: 69.4 or 78.0

Exercises

7.1

\(E_1\)

• LPO(\(g > f\)): \({fgfx \to x, gfx \to fgx, ffgx \to x}\)
• LPO(\(f > g\)): \({fgfx \to x, fgx \to gfx, gffx \to x}\)

\(E_2\)

LPO with arbitrary symbol order: Completion diverges.

Exercises

6.3

\(r_1 = f(r_2)\)

6.4

\(R\) is not confluent. Critical pair in normal form: \(\left < ggfx, fggx \right >\)

\(R' = R \cup {ggfx \to fggx}\). - \(R'\) is confluent: the only new critical pair \(\left < fgggfx, gggx \right >\) is joinable. - \(R'\) terminates: LPO with \(g>f\) proves termination.

6.10

The system is not a term rewrite system, because \(Var(l) \nsupseteq Var(r)\). It is not confluent, because \(f(x)\) has at least two normal forms: \(g(x, g(x, x)\) and \(g(x, g(g(x, x), x)\).

Exercises

2.1.b

Counterexample: \(\to := {(a, c), (b, c)}\)

2.3

\(a \to b\) iff \(a\) encodes Turing machine \(M_a\) and \(b\) encodes a valid terminating computation (sequence of states) of \(M_a\).

2.9

Let \(|w|_a := \varphi_a(w)\).

\(\varphi(w) := 3^{|w|_a} 2^{|w|_b}\)

Proof

1. Let \(u \to_1 v\). Then \(\varphi(v) = 3^{|v|_a} 2^{|v|_b} = 3^{|u|_a+1} 2^{|u|_b-2} = 3^{|u|_a} 2^{|u|_b} \frac{3}{4} = \varphi(u) \frac{3}{4} < \varphi(u)\).
2. Let \(u \to_2 v\). Then \(\varphi(v) = 3^{|v|_a} 2^{|v|_b} = 3^{|u|_a-1} 2^{|u|_b+1} = 3^{|u|_a} 2^{|u|_b} \frac{2}{3} = \varphi(u) \frac{2}{3} < \varphi(u)\).

2.17

No.

Let \(a > b\). Then \([b^n a | n \in [0, 1, \ldots]]\) is an infinite chain according to \(>_{Lex}\).

Note: This exercise completes the discussion of Lemma 2.4.3.

4.2

Let \(s, t\) be terms. Run BFS from \(s\) using \(\leftrightarrow^E\). If \(t\) is encountered, conclude that \(s \approx_E t\). If the BFS finishes enumerating the equivalence class without encountering \(t\), conclude that \(\lnot s \approx_E t\).

4.4

Let \(x \in Var(r) \setminus Var(l)\). Let \(p\) be a position of \(x\) in \(r\).

Infinite chain:

• \(t_0 = x\)
• \(t_{i+1} = r[t_i]_p\)

4.18

1. a
   • Unifier: \({x \to h(a), y \to h(a)}\)
   • Matcher: \({x \to h(a), y \to x}\)
2. b
   • Unifier: Unsolvable
   • Matcher: \({x \to h(x), y \to x}\)
3. c
   • Unifier: \({x \to h(y), z \to b}\)
   • Matcher: Unsolvable
4. d
   • Unifier: Unsolvable
   • Matcher: Unsolvable

5.2

Counterexample TRS \(R\):

1. \(a \to b\)
2. \(b \to b\)

If \(>\) is a rewrite ordering and \(s > t\) for each identity \(s \approx t \in E\), then \(s > t\) for each reduction \(s \to_E t\).

the smaller multiset is obtained from the larger one by removing a nonempty subset \(X\) and adding only elements which are smaller than some element in \(X\).

Source: Term Rewriting and All That, page 22

Schedule

• Week 1: JitPro
• Weeks 2 to 4: Megalodon
• Week 4: Introduction to Coq
• Weeks 5-6: Isabelle, Mizar

``` Definition True : prop := forall p:prop, p -> p. Definition False : prop := forall p:prop, p.

Theorem FalseE: forall A:prop, False -> A. let A. prove False -> A. assume H: False. prove A. prove False. exact H. Qed.

Definition not : prop -> prop := fun A:prop => A -> False.

( Unicode ~ "00ac" ) Prefix ~ 700 := not.

Theorem notE: forall A:prop, not A -> A -> False. let A. prove not A -> A -> False. assume HnA: not A. assume HA: A. prove False. apply HnA. prove A. exact HA. Qed.

Theorem notI: forall A:prop, ( A -> False) -> not A. let A. assume HAF: A -> False. prove not A. exact HAF. Qed.

Definition and : prop -> prop -> prop := fun A B:prop => forall p:prop, (A -> B -> p) -> p.

( Unicode /\ "2227" ) Infix /\ 780 left := and.

Theorem andEL : forall A B:prop, A /\ B -> A. let A B. assume HAB: A /\ B. prove A. apply HAB. prove A -> B -> A. assume HA HB. exact HA. Qed.

Theorem andER : forall A B:prop, A /\ B -> B. let A B. assume HAB: A /\ B. prove B. apply HAB. prove A -> B -> B. assume HA HB. exact HB. Qed.

Theorem andI : forall (A B : prop), A -> B -> A /\ B. let A B. assume HA HB. prove A /\ B. let p. assume HABp: A -> B -> p. prove p. exact HABp HA HB. Qed.

Definition or : prop -> prop -> prop := fun A B:prop => forall p:prop, (A -> p) -> (B -> p) -> p.

( Unicode \/ "2228" ) Infix \/ 785 left := or.

Theorem orE : forall A B C:prop, A \/ B -> (A -> C) -> (B -> C) -> C. let A B C. assume HAB: A \/ B. assume HAC: A -> C. assume HBC: B -> C. prove C. apply HAB. - prove (A -> C). exact HAC. - prove (B -> C). exact HBC. Qed.

Theorem orIL : forall A B:prop, A -> A \/ B. let A B. assume HA: A. prove A \/ B. let p. assume HAp: A -> p. assume HBp: B -> p. prove p. exact HAp HA. Qed.

Theorem orIR : forall A B:prop, B -> A \/ B. let A B. assume HB: B. prove A \/ B. let p. assume HAp: A -> p. assume HBp: B -> p. prove p. exact HBp HB. Qed. ```

What is SType?

Separation

let y. assume Hy : y :e ... prove y :e B. apply ReplE_impred U f y Hy. let x. assume Hx H1. rewrite H1. prove f x :e B.

rewrite matches left hand side and changes its occurrence to right-hand side.

Other direction: rewrite <- H1

Rewrite a particular (for example 2nd) occurrence: rewrite H1 at 2

Alternative: apply (requires a special lambda term)

Related tactic: reflexivity

"impredicative"

Harder to understand, easier to use

exists x, x :e A /\ y = F x

Replacement

Primitives

• Empty set
• Union of set of sets
• Power set
• Repl
• Membership

To assert that we are proving p -> p at this point:

prove p -> p.

Megalodon: assume

Can only be applied on implication.

s [x := t]

x is not free in \(\Gamma\).

Most common case: \(\beta\)-normalize the goal

proposition

https://play.google.com/store/apps/details?id=app.eduroam.geteduroam

\(\Phi X \subseteq X\)

JitPro cheatsheet: JitPro Inference Rules

separation

Sep separates elements from a set.

Let \(\Phi\) be monotone. Let \(Y = {u \in A | \forall X \in P A . \Phi X \subseteq X \to u \in X}\). Then \(\Phi Y \subseteq Y\).

u lies in the intersection of all pre-fixed points of \(\Phi : P(A) \to P(A)\).

fixed-point of \(\Phi : P(A) \to P(A)\)

fixed-point

Set extensionality

\(\Phi\) maps subsets of A to subsets of A.

Repl A F

\(\lambda A B . \forall x \in A . x \in B\)

\(\lambda A . \lambda B . \forall x \in A . x \in B\)

[superfluous word]

\(\frac{P \to Q}{Q \mid \neg P}\)

\(\frac{\neg (P \to Q)}{P, \neg Q}\)

Notation: set is the implicit type.

Additional rules: - Universal quantifier: - \(\forall x . s \models s[x := t]\) - \(\neg \forall x . s \models \neg s[x := y]\) where \(y\) is fresh - Equality: \(s = t, P[s] \models P[t]\)

This is the most common rule.

Also known as Cantor–Bernstein theorem.

Wikipedia: Schröder–Bernstein theorem

Axiom: \(X \subseteq Y \to Y \subseteq X \to X = Y\)

At least one pre-fixed point exists: A.

\(\Phi\) is monotone

Y is a fixed point of \(\Phi\)

800:

Assigned Bandages / Meds / Herbal Meds cannot be taken from a Character in any situation except for the rules written on Fate cards.

Zdroj?

Z \(\phi_1 \circ \phi_2 = id_1\) vyplývá, že \(\phi_1\) je injektivní a \(\phi_2\) je surjektivní.

Srovnej s valuací prvky z nosiče.

Přesnější označení: základní ohodnocení / valuace

Jak víme, že existuje alespoň jedna?

Musíme ale nejdřív zafixovat algebru.

Nejsou. Viz slide 16.

Proč ne raději "\(X = [X_d]_{d \in D}\) pro každý druh"?

Musí být každá \(\Sigma_\tau\) konečná?

Aby bylo možné signaturu zapsat konečným řetězcem, musí být každá \(\Sigma_\tau\) konečná.

AKA magma

https://en.wikipedia.org/wiki/Magma_(algebra)

The operation is partial because not every pair of paths can be concatenated. Two paths can only be concatenated if the target of the first one coincides with the source of the second one.

empty set

Nat

• A team that
  • doesn’t understand formal methods,
  • has only a notion of what they specified using a formal notation, and
  • is unclear about how to refine the development process,
• will almost certainly sink the project.

Generický?

Czech translation: https://www.voxpot.cz/vase-schopnost-soustredeni-se-nezhroutila-byla-ukradena/

https://guardianbookshop.com/stolen-focus-9781526620224

http://williams.nu/

Slides

Evaluation from the teacher:

Your grade for your presentation was a B+. Your visuals were quite good, your information was interesting, and your verbal delivery was very solid. Your non-verbal communication, however, had some issues, especially with eye contact and engaging with the audience. These are things that will continue to improve with practice, however. Overall, good work.

Planned topic: Univalent Foundations

def curry (α β γ : Type*) (f : α × β → γ) : α → β → γ := λ a b, f (a, b)
def uncurry (α β γ : Type*) (f : α → β → γ) : α × β → γ := λ p, f p.1 p.2

2021-11-04

• Komodita: zemní plyn
• Jednotka: Kč/MWh
• Aktuální graf: https://www.tzb-info.cz/ceny-paliv-a-energii

• Komodita: elektřina
• Jednotka: Kč/MWh
• Aktuální graf: https://www.tzb-info.cz/ceny-paliv-a-energii

This characteristic is only used for problems all of whose atoms are equalities.

Krajicek:

We take turns in lecturing.

Next Friday I will lay out the questions we will be interested in. We will discuss who will talk about what.

Browse through the Xena materials.

Larch https://thelarch.notion.site/thelarch/Larch-73c9d52748e64d4b83e2812e458b7c44

This lecture is canceled.

concept equivalence

https://openai.com/blog/clip/

• https://scholarphi.org/
• https://www.semanticscholar.org/product/semantic-reader

15:30-15:50

Raises:

• ValueError if
  • a hyperparameter (HP) instantiation is illegal,
  • an active HP is not specified, or
  • an inactive HP is specified.
• ConfigSpace.exceptions.ForbiddenValueError if a forbidden clause is violated.

Source: ConfigSpace/c_util.pyx

Empirical perfromance model

http://cl-informatik.uibk.ac.at/users/swinkler/arcade2021/

http://cl-informatik.uibk.ac.at/users/swinkler/arcade2021/

Srovnej: tatíček Masaryk, praotec Čech

Promítaly se filmy:

1. Acid Rain
2. Takové pěkné město
3. M E Z E R Y
4. Divoké bytosti

https://www.brno16.cz/pages/competitions

Special characters:

.^$*+?{}\[]|()

Supported values:

• quality
• runtime

https://en.wikipedia.org/wiki/Hedge_fund