481 Matching Annotations
  1. Feb 2024
  2. Dec 2023
  3. Nov 2023
    1. Let me take up first the requirements imposed on the teacher and then go on to those placed on the pupil. Once a student of mine, endeavoring to reproduce a Socratically conducted exercise, presented a version in which he put the replies now into the teacher's mouth, now into the pupil's. Only my astonished question, "Have you ever heard me say 'yes' or 'no'?" stopped him short. Thrasymachus saw the point more clearly; in Plato's Republic he calls out to Socrates: "Ye gods! . . . I knew it . . . that you would refuse and do anything rather than answer" [Plato, The Republic, Paul Shorey, tr., in Loeb Classical Library, London, New York, p.41]. The teacher who follows the Socratic model does not answer. Neither does he question. More precisely, he puts no philosophical questions, and when such questions are addessed to him, he under no circumstances gives the answer sought. Does he then remain silent? We shall see. During such a session we may often hear the despairing appeal to the teacher:  "I don't know what it is you want!" Whereupon the teacher replies: "I? I want nothing at all." This certainly does not convey the desired information. What is it, then, that the teacher actually does? He sets the interplay of question and answer going between the students, perhaps by the introductory remark: "Has anyone a question?" Now, everyone will realize that, as Kant said, "to know what questions may reasonably be asked is already a great and necessary proof of sagacity and insight" [Kant, Critique of Pure Reason, p.97]. What about foolish questions, or what if there are no questions at all? Suppose nobody answers? You see, at the very beginning the difficulty presents itself of getting the students to the point of spontaneous activity, and with it arises the temptation for the teacher to pay out a clue like Ariadne's thread. But the teacher must be firm from the beginning, and especially at the beginning. If a student approaches philosophy without having a single question to put to it, what can we expect in the way of his capacity to persevere in explorin its complex and profound problems? What should the teacher do if there are no questions? He should wait -- until questions come. At most, he should request that in the future, in order to save time, questions be thought over in advance. But he should not, just to save time, save the students the effort of formulating their own questions. If he does, he may for the moment temper their impatience, but only at the cost of nipping in the bud the philosophical impatience we seek to awaken. Once questions start coming -- one by one, hesitantly, good ones and foolish ones -- how does the teacher receive them, how does he handle them? He now seems to have easy going since the rule of the Socratic method forbids his answering them. He submits the questions to discussion. All of them? The appropriate and the inappropriate? By no means. He ignores all questions uttered in too low a voice. Likewise those that are phrased incoherently. How can difficult ideas be grasped when they are expressed in mutilated language? Thanks to the extraordinary instruction in the mother tongue given in our schools, over half I the questions are thus eliminated [note]. As for the rest, many are confused or vague. Sometimes clarification comes with the counterquestion:  "Just what do you mean by that?" But very often this will not work because the speaker does not know what he means himself. The work of the discussion group thus tends automatically either to take up the clear, simple questions or to clear up unclear, vague ones first.

      Common search for a philosophical question

    2. If we inquire into the conditions of their possibility, we come upon more general propositions that constitute the basis of the particular judgments passed. By analyzing conceded judgments we go back to their presuppositions. We operate regressively from the consequences to the reason. In this regression we eliminate the accidental facts to which the particular judgment relates and by this separation bring into relief the originally obscure assumption that lies at the bottom of the judgment on the concrete instance. The regressive method of abstraction, which serves to disclose philosophical principles, produces no new knowledge either of facts or of laws. It merely utilizes reflection to transform into clear concepts what reposed in our reason as an original possession and made itself obscurely heard in every individual judgment.

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

  4. Oct 2023
    1. 20 812

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

  5. Sep 2023
    1. Sean B. Holden

      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."

  6. Aug 2023
    1. Synod ČCE souhlasí s možností požehnání svazků osob stejného pohlaví, pokud o to požádají. Synod ČCE vnímá, že názory na tuto otázku nejsou v církvi jednotné, podporuje činnost komise pro soužití s LGBTQ lidmi a pokračování diskuze v církvi o tomto tématu. Synod konstatuje, že žádný kazatel není povinen žehnat svazkům osob stejného pohlaví.
    1. body v čase

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

    2. dobře zapamatovaný

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

    3. EMOČNĚ „UZAVŘENÝ“

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

    4. odpověďna hlavní otázku rozhovoru je skryta v jeho příkladu

      Co přesně tohle znamená?

    5. není během rozhovoru možné pracovat s hypotetickými situa-cemi nebo se snažit dohadovat „co kdyby“.

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

  7. Jul 2023
    1. jistého rekreačního zařízení
    2. Skupina začne sdílením svých zkušeností, potom si jednu vybere a teprve pak formu-luje otázky, na které by ráda pomocí vybrané zkušenosti odpověděla.

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

    3. nejprve musíme vybrat a připravit hlavní téma nebo otázku

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

    4. udržet si zdravou míru pochybování a zároveň otevřenostinahlížet věci jinak

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

    5. Je velmi cenné, když účastník během prvních sezení zastává nějakýsvůj názor, a pak si uvědomí, že jej změnil.

      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.

    6. diskuzi

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

    Tags

    Annotators

  8. Mar 2023
  9. Feb 2023
    1. 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.

  10. Oct 2022
    1. Automated Reinforcement Learning

      2022-10-13 16:00

    2. Dynamic Selection and Configuration of Optimization Algorithms: From Hyperparameter Control to AutoML

      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

    3. User-Priors for Hyperparameter Optimization

      https://tinyurl.com/2p9fm8z6

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

    4. Recommender Systems for AutoML & AutoML for Recommender Systems

      Links

      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.

    5. On the Automation of Data Science

      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

    1. AutoML for diverse tasks: cf. general game playing

      automl.decathlon@gmail.com

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

    1. datasets

      H2O only supports tabular datasets.

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

    3. Code will be provided, which can be used to automatically train and explain models on your own datasets.
    1. 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
  11. Sep 2022
    1. Efficient Neural Clause Selection by Weight

      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?

    2. Evolutionary Computation for Program Synthesis in SuSLik
    3. Walter Dean and Alberto Naibo

      philosophers, logicians

    4. A modular reinforcement learning based automated theorem prover

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

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

    5. Elements of Reinforcement Learning in Saturation-based Theorem Proving

      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.

    6. Proving Theorems using Incremental Learning and Hindsight Experience Replay

      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.

    7. Forbidden Substructure Theorems

      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.

  12. Jun 2022
  13. May 2022
    1. One ATP system runs on one CPU at a time, with access to half (128GB) the memory.

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

    2. Intel(R) Xeon(R) E5-2667
    1. Special Variables

      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.

  14. Apr 2022
    1. Všichni "odborníci" se shodují, že vakcíny zabraňují těžkému průběhu Covid-19. Jen data jim to trochu kazí... (Anglie Covid úmrtí leden 2022. Zelená neočko, červená očko 2 dávky.)

      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

  15. Mar 2022
    1. 7 Completion

      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.

    2. 6 Confluence

      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)\).

    3. 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\)
    1. rewrite ordering

      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\).

    2. there exist X, Y ∈ Mult(M ) with X 6 = ∅, X ⊆A, B = (A\X) ∪ Y , and for all y ∈ Y exists an x ∈ X withx > y.

      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

    1. Schedule

      • Week 1: JitPro
      • Weeks 2 to 4: Megalodon
      • Week 4: Introduction to Coq
      • Weeks 5-6: Isabelle, Mizar
    2. A few simple basic logic exercises in Megalodon: Basic Logic Exercises

      ``` 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. ```

  16. grid01.ciirc.cvut.cz grid01.ciirc.cvut.cz
    1. SType

      What is SType?

    2. Sep

      Separation

    3. admit. (** fill in the rest of this proof **)

      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

    4. ReplE_impred

      "impredicative"

      Harder to understand, easier to use

    5. exists x :e A, y = F x

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

    6. Repl

      Replacement

    7. Set Theory

      Primitives

      • Empty set
      • Union of set of sets
      • Power set
      • Repl
      • Membership
    8. assume Hp: p.

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

      prove p -> p.

    9. →I Γ, s ` tΓ ` s → t

      Megalodon: assume

      Can only be applied on implication.

    10. sxt

      s [x := t]

    11. x ∈ Vα \ FΓ

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

    12. Conv Γ ` sΓ ` t s≈t

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

    13. o is also written prop.

      proposition

    1. X is a pre-fixed point

      \(\Phi X \subseteq X\)

    2. JitPro cheatsheet: JitPro Inference Rules

    3. Object. The name Sep is a term of type set → (set → prop) → set.

      separation

      Sep separates elements from a set.

    4. Subgoal 1

      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\).

    5. lpfp A Φ u

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

    6. fp A Φ

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

    7. fp

      fixed-point

    8. Known. (set_ext)

      Set extensionality

    9. (∀U ∈ 𝒫 A, Φ U ∈ 𝒫 A)

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

  17. Feb 2022
    1. {F x|x ∈ A}

      Repl A F

    2. λA B ⇒ ∀x ∈ A, x ∈ B

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

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

    3. when

      [superfluous word]

    4. If P → Q is on the branch, then we can split into two subgoals to refute given by two extended branches: one extended by Q and the other extended by ¬ P

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

    5. If ¬ (P → Q) is on the branch, then we can extend the branch with P and ¬ Q.

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

    6. set

      Notation: set is the implicit type.

    7. Tableau Refutations

      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]\)

    8. Negated Implication

      This is the most common rule.

    9. Theorem: Schroeder Bernstein

      Also known as Cantor–Bernstein theorem.

      Wikipedia: Schröder–Bernstein theorem

    10. set extensionality

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

    11. pre-fixed point

      At least one pre-fixed point exists: A.

    12. (∀U V ∈ 𝒫 A, U ⊆ V → Φ U ⊆ Φ V)

      \(\Phi\) is monotone

    13. Φ Y = Y

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

    1. Meds/Bandages/Herbal Meds not referred to on Fate cards are returned to the Storage.

      800:

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

  18. Jan 2022
    1. platí1 ₒ 2 = id1 . Podobně i obráceně 2 ₒ 1 = id2

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

    2. valuace proměnných z tkonstantními výrazy

      Srovnej s valuací prvky z nosiče.

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

    3. Pro každou algebraickou specifikaci S = (D, , E), existuje právě jednatřída iniciálních algeber ve třídě všech modelů specifikace S.

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

    4. Každou valuaci lze jednoznačně rozšířit na zobrazení ’: T(X)  A .

      Musíme ale nejdřív zafixovat algebru.

    5. Jsou tyto modely isomorfní?

      Nejsou. Viz slide 16.

    6. X = [X]T pro každý typ

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

    7. množin 

      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á.

    8. grupoid
    1. partial concatenation operation

      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.

    1. A team that doesn’tunderstand formal methods has only a notion of whatthey specified using a formal notation and is unclearabout how to refine the development process will almostcertainly sink the project.
      • 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.
    1. Filip Bártek

      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.

  19. Dec 2021
  20. Nov 2021
    1. def curry (α β γ : Type*) (f : α × β → γ) : α → β → γ := sorry def uncurry (α β γ : Type*) (f : α → β → γ) : α × β → γ := sorry
      def curry (α β γ : Type*) (f : α × β → γ) : α → β → γ := λ a b, f (a, b)
      def uncurry (α β γ : Type*) (f : α → β → γ) : α × β → γ := λ p, f p.1 p.2
      
  21. Oct 2021
    1. Vývoj cen na spotovém vnitrodenním trhu Operátora trhu za posledních dvanáct měsíců
    2. Vývoj cen na spotovém denním trhu Operátora trhu za posledních dvanáct měsíců
    1. EQU (with equality)

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

    1. 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.

  22. Sep 2021
    1. Creation of a modular proof assistant engine for a logic e-tutor
    2. Computer Verification for Historians of Philosophy

      This lecture is canceled.

    3. Cryptomorphism

      concept equivalence

    4. Contrastive finetuning of generative language models for informal premise selection
    5. Mathematics in the Scholarly Literature
    6. Filip Bártek and Martin Suda Project Proposal: Model-Based Optimization of Strategy Schedules (20m)

      15:30-15:50

    1. an error

      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

  23. Jul 2021
  24. Jun 2021
    1. Krátké animované filmy z festivalu B16

      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

  25. May 2021
    1. i učitelé mají dobrou paměť a studenty, kteří výuku tak nějak flinkají, obvykle, i přes celou řadu slibů, vést nechtějí

      zbytečná moralizace

    1. Začátkem práce na tvorbě textu končí období, které jsme věnovali přípravě podkladů, tvorbě výstupů, provedení rešerší a dalších činností, které vycházely ze zadání závěrečné práce.
    2. téměř vždy je na vině student

      zbytečná moralizace

  26. Apr 2021
  27. Mar 2021
    1. X⊥⊥Z|Y[π],thenπ(X,Y,Z)canb ereconstructedfromπ↓{X,Y}andπ↓{Y,Z}usingEquation(1.1).

      $$ \pi(x,y,z) = \frac{\pi(x,y) \pi(y,z)}{\pi(y)} = \frac{\pi(x,y) \pi(y,z)}{\sum_{x' \in \mathbb{X}_X} \pi(x',y)} $$

  28. Nov 2020
  29. Oct 2020
    1. Symmetry breaking

      Two propositional variables are symmetrical iff exchanging them leads to the same problem. Their identity carries no relative value.

    1. Difference logic

      Why are there no propositional operations?

    2. EUF

      Theory of Equality and Uninterpreted Functions

    3. if𝜙′/∈SAT, then return𝜙 /∈SAT

      The first SAT is propositional. The second SAT is modulo T.

    1. How does the meaning of the formula change if you replace(𝑥𝑛∨𝑦𝑛∨𝑎𝑛−1)by(𝑥𝑛∨𝑎𝑛−1)∧(𝑦𝑛∨𝑎𝑛−1)?

      The inequality becomes strict.

    2. What is the purpose of auxiliary variables?

      Let's assume that \(a_0 = 1\). Let \(j\) be the smallest index such that \(x_j \neq y_j\). Then \(a_i = 1\) for all \(i < j\).

      • If \(x_j > y_j\), then the formula is unsatisfiable.
      • If \(x_j < y_j\), then \(a_i\) is unconstrained for all \(i \geq j\).

      \(a_i\) is forced to 1 iff \(x\) and \(y\) are constrained at index \(i\).

    3. Why can we replace(𝑥𝑛∨𝑦𝑛∨𝑎𝑛−1)∧(𝑥𝑛∨𝑎𝑛∨𝑎𝑛−1)∧(𝑦𝑛∨𝑎𝑛∨𝑎𝑛−1)just by(𝑥𝑛∨𝑦𝑛∨𝑎𝑛−1)? Hence we need only3𝑛−2clauses and𝑛−1auxiliary variables (𝑎𝑛is also useless)

      The only purpose of \(a_i\) is to signal to the higher indices of \(x\) and \(y\) whether they are constrained.

    4. Why is𝑎0always false and hence useless?

      We must constrain \(a_0\) to 1. Otherwise the whole formula is satisfied by \(a_i = 0\) for all \(i\).

    1. How to encode typical constraints
    2. hard—must be satisfied

      This seems to be possible to implement with transfinite weights.

    3. 𝑝

      Usually \(p < 0.5\).

    4. Unary encoding (order encoding)

      Makes expressing inequalities easy:

      • \(x < i \leftrightarrow \overline{x_i}\)
      • \(x \geq i \leftrightarrow x_i\)
    5. while𝜙contains a pure literal𝑙dodelete clauses containing𝑙from𝜙

      In practice pure literal elimination is usually not used because it does not work efficiently with the data structures used to keep track of unit clauses.

    1. There are few exercises in this unit and all of them are voluntary (only intended for inexperienced students).

    1. Acronyms are all right as long as they are defined explicitly first, for example:

      personal protective equipment (PPE)

    2. Oxford comma”

      Oxford comma is useful especially when a list item contains "and", for example:

      One, two and three, and four.

  30. Sep 2020
    1. If not, you must pick up the discard pile.

      Do I get to pick the card I just flipped over as well?

    1. DO NOT use etc., i.e., or e.g.

      Michael: It is ok to use these short forms in brackets.

    2. hedging

      What exactly is hedging? What does it look like?

    3. Be non-personal

      How should I deal with sentences such as:

      we restrict our attention to learning precedences for predicate symbols only

      In this work, we design a system [...]

      We call the vector w the coefficients [...]

      Source: https://github.com/filipbartek/learning-precedences-from-elementary-symbol-features/releases/download/paar2020%2Fceur-2/Learning_Precedences_from_Simple_Symbol_Features.pdf

    4. and / or

      "and / or" does not seem to be an adequate substitute for "etc." to me.

    1. Punctuation in Academic Writing

      Punctuation is governed by style guides. When writing for a journal, ask them what style guide they follow.

    1. Michael prefers the participants to have their video enabled.

      Homework assignments:

      1. Introduction (paragraph or section)
      2. Body (paragraph or section)
    1. monotone

      monotonic

    2. Two formulae𝜙and𝜓are equivalent, we write𝜙≡𝜓or𝜙|=|𝜓

      Cf. "equisatisfiable"

    3. (𝜙1∧···∧𝜙𝑛)→(𝜓1∨···∨𝜓𝑚)

      Special example: Horn clauses

    4. 𝜙follows from(oris a consequence of)a formula𝜓

      \(\psi\) entails \(\phi\)

    5. all valid formulae are derivable (provable)

      valid -> derivable

    6. only valid formulae are derivable (provable)

      derivable -> valid

    7. Examples of used formal systems

      Not to be discussed in this course:

      • QBF
      • modal logics
      • HOL
    8. British Museum algorithm

      Random search

    9. foundations of mathematics in the late 19thcentury and early 20th century

      Cf. Hilbert's program

    10. derive (prove) formulae

      provability

    11. semantic consequence.

      entailment

    12. {𝑥:𝑥 /∈𝑥}

      How to define a set? For example by set comprehension, as exemplified here.

    1. The course extends on some previous courses. Namely we discuss computational aspects of inference.

      Filip Zelezny: The lectures are to be recorded by the students.

      Karel Chvalovsky: Feel free to unmute yourself and ask questions, or write them in the chat.

    2. First-order resolution

      We rely on theoretical knowledge of e.g. resolution from previous courses and we focus on computation hacks.

    3. Proof assistants

      Is this lecture focused at high-order logic?

    4. 9 23.11. Chvalovský Answer set programming 10 30.11. Chvalovský First-order logic 11 7.12. Chvalovský First-order resolution 12 14.12. Chvalovský Equality and model finding 13 4.1. Chvalovský Proof assistants

      These approaches are more modern than Prolog.

    5. Prolog

      Logical programming is not as important nowadays as it used to be. It is currently not fashionable.

      Filip: Why not use OCaml instead?

      Prolog is an example of declarative programming language.

    6. SAT solving

      Improving SAT solvers leads to making many NP-complete problems easier to solve computationally.

  31. Aug 2020
    1. the place value of the "hundreds" digit in base seven is 49

      I don't understand.

    1. Node List

      How to print the info:

      sinfo -o "%9n %9P %.4c %.6m %.8d %14f %G"
      

      How to format with xsv:

      sinfo -o "%n|%P|%c|%m|%d|%f|%G" | xsv table --delimiter "|"
      
  32. Jun 2020
    1. Unfortunately

      I consider it rather fortunate since it allows me to clean up, as demonstrated below.

    1. "There was a 0.95 correlation. I asked them about it. They said, 'We read this article in Chain Store Age magazine that said beer and diapers are correlated, so we put beer next to diapers in all of our stores," he said. "What they did was they created the data that actually validates the data. In effect, they created the signal they used to validate the signal."

      Placement of the goods is a confounder.

  33. May 2020
  34. Apr 2020
    1. Zaměstnanci s emailovou adresou ve formátu: jmeno.prijmeni@cvut.cz

      Configuration that works in Thunderbird in English in Ubuntu:

      • Incoming:
        • Authentication: Normal password
        • Username: bartefil
      • Outgoing:
        • Authentication: Normal password
        • Username: bartefil
  35. Feb 2020
    1. fisk.pdf(x, c, loc, scale)
      y = (x - loc) / scale
      return c * np.power(y, -c-1) * np.power(1 + np.power(y, -c), -2) / scale
      
  36. Jan 2020
    1. Which core is the best to emulate(some console/game)?

      Emulation General Wiki contains comparisons of emulators of various platforms.

  37. Dec 2019