- Sep 2024
-
www.mercusys.com www.mercusys.com
-
Keep the router away from microwave ovens and other interference sources (refrigerators, ovens, Bluetooth devices, etc.) Reduce the number of wireless clients and optimize the router’s position. Try to adjust the orientation of the antennas for maximum performance. We recommend placing it as the same height with wireless clients and also placing its antennas at 45 degrees or 0 degrees (parallel to the floor) to the floor, which will be more effective. Since antennas always transmit weakly at the base, do not place your wireless client device at the bottom of Mercusys wireless device. If your Wi-Fi's signal strength is weak, try moving the router to another location. Minimize obstructions between your router and your computer or other devices. Obstructions such as walls between your router and device can affect Wi-Fi signal quality.
-
-
-
Měsíční poplatek vypočítáte pomocí tohoto vzorce: 14,33 Kč × počet ampérů hlavního jističe. V případě, že máte domácnost připojenou třífázově, výsledek ještě vynásobte třemi (týká se to především rodinných domů). Výše poplatku má omezenou horní hranici, která je ze zákona maximálně 599 Kč včetně DPH za spotřebovanou megawatthodinu. Tato horní hranice se týká většiny běžných spotřebitelů.
Aktuální poplatek: max. 495 Kč/MWh
-
-
www.deepsy.cz www.deepsy.czDeePsy1
-
Code that reads and aggregates individual measurements: https://colab.research.google.com/drive/1ga25tsi2MMQ-zBdFLyO_ICqbB39IMrVD
-
- Aug 2024
-
plato.stanford.edu plato.stanford.edu
-
neither p nor q
$$\lnot p \land \lnot q$$
-
monadic first-order logic
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
-
- Jul 2024
-
plato.stanford.edu plato.stanford.edu
-
xy=x
$$\forall i : x(i) \land y(i) \Leftrightarrow x(i)$$
What would suffice: $$\forall i : x(i) \Rightarrow y(i)$$
-
-
www.springer.com www.springer.com
-
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
-
-
easychair.org easychair.orgProgram3
-
-
Regularization in Spider-style Strategy Discovery and Schedule Construction
-
Logically Constrained Rewrite Systems
LCTRS
-
- Jun 2024
-
monosphereband.bandcamp.com monosphereband.bandcamp.com
-
killswitch
-
We were born to run through mazes Our minds were designed to escape
AI systems trained by reinforcement learning are sometimes trained on maze-like tasks.
-
Through the ebb and flow Wondering where’d you go Shining bright It’s too late to fall apart
The riff resembles the riff in the verse "The only one I loved was you" in The Lover.
-
-
metastavy.bandcamp.com metastavy.bandcamp.com
-
a
Na
-
i když
přestože
Tags
Annotators
URL
-
- Apr 2024
-
resource-cms.springernature.com resource-cms.springernature.comTitel1
-
Captions that donot constitute a full sentence, do not have a period.
According to this document, "[t]he last sentence of a [...] caption should end without a period".
-
- Mar 2024
-
europroofnet.github.io europroofnet.github.io
-
Learning to Rank in Automatic Theorem Proving
Extended abstract and slides: https://github.com/filipbartek/wg5-vienna24/releases/tag/final
-
A practical application of machine learning in Vampire
How do you generate the training data? How do you vary the encoding (direct vs. indirect)?
-
Neural Termination Analysis
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
- Train a NN
- 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.
-
Integrating ML into SMT solvers
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?
-
Neuro-Symbolic Specification Generation for C programs
What is a perfect specification? One that exactly describes the behavior of the program as a black box.
-
Guiding Enumerative Program Synthesis with Large Language Models
Paper: https://arxiv.org/abs/2403.03997v1
With A* enumeration, what is the target of the search and how is the distance computed?
-
26th March
0930–1000 Alessandro Bruni: [formalization of probability theory in Coq] - MathComp-Analysis
-
Exploration of properties of differentiable logics through mechanisation
- Why can we disregard the left hand side of the property?
- Do you always "fix" the NN using a particular sample and property?
-
Algorithm Selection for Symbolic Integration using Machine Learning
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.
-
1200–1230
Actual start: 11:30
-
Machine Learning for Automated Theorem Proving: an ML-side perspective
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)
-
- Feb 2024
-
theconversation.com theconversation.com
-
St. John’s Passion: Part 1 – Herr, unser Herrscher
-
-
www.voxpot.cz www.voxpot.cz
-
GOP
Grand Old Party – Republikánská strana
-
- Dec 2023
-
-
In the figure "Years needed to buy a 75-square-meter flat", what is the source of the apartment prices?
-
- Nov 2023
-
friesian.com friesian.com
-
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
-
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.
-
- Oct 2023
-
www.mpsv.cz www.mpsv.cz
-
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č.
-
- Sep 2023
-
-
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."
-
- Aug 2023
-
www.heroine.cz www.heroine.cz
-
vytvořil z ženských sportovkyň, které již nešlo ignorovat, „druhou kategorii“
Zdroj?
-
-
synod.e-cirkev.cz synod.e-cirkev.cz
-
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í.
-
-
Local file Local file
-
body v čase
Jak pracujeme s chronologií? Je chronologie důležitá?
-
dobře zapamatovaný
Jak v sokratovském rozhovoru pracujeme s nedokonalostí paměti a domýšlením ("filling in the gaps")?
-
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
-
odpověďna hlavní otázku rozhovoru je skryta v jeho příkladu
Co přesně tohle znamená?
-
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.
-
-
furtherdown.bandcamp.com furtherdown.bandcamp.com
- Jul 2023
-
Local file Local file
-
jistého rekreačního zařízení
Jedná se o Rekreační a školící středisko Loutí?
-
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".
-
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.
-
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?
-
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.
-
diskuzi
Jaký je rozdíl mezi rozhovorem a diskuzí?
-
- Mar 2023
-
cw.fel.cvut.cz cw.fel.cvut.cz
-
Foundations of Machine Learning
-
- Feb 2023
-
www.smartgames.eu www.smartgames.eu
-
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:
- Inspection ("look"): Inspect the challenge without touching any piece. Try to invent a plan of moving the pieces to solve the challenge.
- 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.
-
- Oct 2022
-
sites.google.com sites.google.com
-
Automated Reinforcement Learning
2022-10-13 16:00
-
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
-
User-Priors for Hyperparameter Optimization
\(\pi\)BO is implemented in HyperMapper.
-
Recommender Systems for AutoML & AutoML for Recommender Systems
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
- Rating prediction
- Top-n ranking
AutoRecSys
Several rating prediction libraries exist. They focus on CASH (... algorithm selection ...) problem.
-
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
Data exploration
De Bie: Subjective interestingness (contrast with the data analyst's prior expectations)
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
-
-
sites.google.com sites.google.com
-
AutoML for diverse tasks: cf. general game playing
automl.decathlon@gmail.com
Deadline for competitions: 2022-10-13 12:30
-
-
sites.google.com sites.google.com
-
-
cs.lth.se cs.lth.se
-
ninja developer
For example Andrej Karpathy
-
-
sites.google.com sites.google.com
-
sites.google.com sites.google.com
-
tickets for public transport for 4 days
-
-
sites.google.com sites.google.com
-
datasets
H2O only supports tabular datasets.
-
What makes the training nondeterministic: - Neural networks with more than 1 worker - Wallclock time limit
-
Code will be provided, which can be used to automatically train and explain models on your own datasets.
-
-
sites.google.com sites.google.com
-
How can Gaussian process be used with categorical variables?
-
-
www.uroboros.design www.uroboros.design
-
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
-
- Sep 2022
-
aitp-conference.org aitp-conference.org
-
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?
-
Evolutionary Computation for Program Synthesis in SuSLik
-
Walter Dean and Alberto Naibo
philosophers, logicians
-
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
-
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.
-
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.
-
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.
-
- Jun 2022
-
archiv.hn.cz archiv.hn.cz
-
www.tptp.org www.tptp.org
-
Computers
-
octa
8
-
- May 2022
-
www.tptp.org www.tptp.org
-
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
-
Intel(R) Xeon(R) E5-2667
-
-
wiki.uiowa.edu wiki.uiowa.edu
-
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.
-
-
zivotastrom.cz zivotastrom.cz
-
Původní transparentní účet: https://www.csas.cz/cs/transparentni-ucty#/000000-4482788379
-
- Apr 2022
-
antivirus.22web.org antivirus.22web.org
-
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
-
- Mar 2022
-
www21.in.tum.de www21.in.tum.de
-
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.
-
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)\).
-
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
- 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)\).
- 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
- a
- Unifier: \({x \to h(a), y \to h(a)}\)
- Matcher: \({x \to h(a), y \to x}\)
- b
- Unifier: Unsolvable
- Matcher: \({x \to h(x), y \to x}\)
- c
- Unifier: \({x \to h(y), z \to b}\)
- Matcher: Unsolvable
- d
- Unifier: Unsolvable
- Matcher: Unsolvable
5.2
Counterexample TRS \(R\):
- \(a \to b\)
- \(b \to b\)
-
-
wwwlehre.dhbw-stuttgart.de wwwlehre.dhbw-stuttgart.de
-
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\).
-
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
-
-
grid01.ciirc.cvut.cz grid01.ciirc.cvut.cz
-
Schedule
- Week 1: JitPro
- Weeks 2 to 4: Megalodon
- Week 4: Introduction to Coq
- Weeks 5-6: Isabelle, Mizar
-
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. ```
-
-
grid01.ciirc.cvut.cz grid01.ciirc.cvut.czsbmg.pdf13
-
SType
What is SType?
-
Sep
Separation
-
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
-
ReplE_impred
Harder to understand, easier to use
-
exists x :e A, y = F x
exists x, x :e A /\ y = F x
-
Repl
Replacement
-
Set Theory
Primitives
- Empty set
- Union of set of sets
- Power set
- Repl
- Membership
-
assume Hp: p.
To assert that we are proving
p -> p
at this point:prove p -> p.
-
→I Γ, s ` tΓ ` s → t
Megalodon:
assume
Can only be applied on implication.
-
sxt
s [x := t]
-
x ∈ Vα \ FΓ
x is not free in \(\Gamma\).
-
Conv Γ ` sΓ ` t s≈t
Most common case: \(\beta\)-normalize the goal
-
o is also written prop.
proposition
-
-
ist.cvut.cz ist.cvut.cz
-
Aplikaci geteduroam si stáhnete z obchodu Google Play.
-
-
grid01.ciirc.cvut.cz grid01.ciirc.cvut.cz
-
X is a pre-fixed point
\(\Phi X \subseteq X\)
-
JitPro cheatsheet: JitPro Inference Rules
-
Object. The name Sep is a term of type set → (set → prop) → set.
separation
Sep separates elements from a set.
-
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\).
-
lpfp A Φ u
u lies in the intersection of all pre-fixed points of \(\Phi : P(A) \to P(A)\).
-
fp A Φ
fixed-point of \(\Phi : P(A) \to P(A)\)
-
fp
fixed-point
-
Known. (set_ext)
Set extensionality
-
(∀U ∈ 𝒫 A, Φ U ∈ 𝒫 A)
\(\Phi\) maps subsets of A to subsets of A.
-
- Feb 2022
-
grid01.ciirc.cvut.cz grid01.ciirc.cvut.cz
-
{F x|x ∈ A}
Repl A F
-
λ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\)
-
when
[superfluous word]
-
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}\)
-
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}\)
-
set
Notation: set is the implicit type.
-
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]\)
-
Negated Implication
This is the most common rule.
-
Theorem: Schroeder Bernstein
Also known as Cantor–Bernstein theorem.
Wikipedia: Schröder–Bernstein theorem
-
set extensionality
Axiom: \(X \subseteq Y \to Y \subseteq X \to X = Y\)
-
pre-fixed point
At least one pre-fixed point exists: A.
-
(∀U V ∈ 𝒫 A, U ⊆ V → Φ U ⊆ Φ V)
\(\Phi\) is monotone
-
Φ Y = Y
Y is a fixed point of \(\Phi\)
-
-
boardgamegeek.com boardgamegeek.com
-
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.
-
- Jan 2022
-
www.voxpot.cz www.voxpot.cz
-
Jenže ti mohou chybovat a některá videa proklouznou.
Zdroj?
-
-
moodle.fel.cvut.cz moodle.fel.cvut.cz
-
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í.
-
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
-
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?
-
Každou valuaci lze jednoznačně rozšířit na zobrazení ’: T(X) A .
Musíme ale nejdřív zafixovat algebru.
-
Jsou tyto modely isomorfní?
Nejsou. Viz slide 16.
-
X = [X]T pro každý typ
Proč ne raději "\(X = [X_d]_{d \in D}\) pro každý druh"?
-
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á.
-
grupoid
AKA magma
-
-
maude.lcc.uma.es maude.lcc.uma.es
-
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.
-
-
moodle.fel.cvut.cz moodle.fel.cvut.cz
-
none
empty set
-
Bool
Nat
-
-
moodle.fel.cvut.cz moodle.fel.cvut.cz
-
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.
- A team that
-
-
moodle.fel.cvut.cz moodle.fel.cvut.cz
-
zásobníkový počítač
Generický?
-
-
www.theguardian.com www.theguardian.com
-
-
Stolen Focus: Why You Can’t Pay Attention
-
James Williams
-
-
moodle.fel.cvut.cz moodle.fel.cvut.cz
-
Filip Bártek
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.
-
- Dec 2021
-
www2.karlin.mff.cuni.cz www2.karlin.mff.cuni.cz
-
17.XII.2021, Claudia Ligonie Lerma, tba
Planned topic: Univalent Foundations
-
- Nov 2021
-
leanprover.github.io leanprover.github.io
-
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
-
- Oct 2021
-
moodle.fel.cvut.cz moodle.fel.cvut.cz
-
Lesson 6: Individual Consultations
2021-11-04
-
-
www.tzb-info.cz www.tzb-info.cz
-
Vývoj cen na spotovém vnitrodenním trhu Operátora trhu za posledních dvanáct měsíců
- Komodita: zemní plyn
- Jednotka: Kč/MWh
- Aktuální graf: https://www.tzb-info.cz/ceny-paliv-a-energii
-
Vývoj cen na spotovém denním trhu Operátora trhu za posledních dvanáct měsíců
- Komodita: elektřina
- Jednotka: Kč/MWh
- Aktuální graf: https://www.tzb-info.cz/ceny-paliv-a-energii
-
-
www.tptp.org www.tptp.org
-
EQU (with equality)
This characteristic is only used for problems all of whose atoms are equalities.
-
-
www2.karlin.mff.cuni.cz www2.karlin.mff.cuni.cz
-
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.
-
- Sep 2021
-
aitp-conference.org aitp-conference.org
-
Creation of a modular proof assistant engine for a logic e-tutor
-
Computer Verification for Historians of Philosophy
This lecture is canceled.
-
Cryptomorphism
concept equivalence
-
Contrastive finetuning of generative language models for informal premise selection
-
Mathematics in the Scholarly Literature
-
Filip Bártek and Martin Suda Project Proposal: Model-Based Optimization of Strategy Schedules (20m)
15:30-15:50
-
-
automl.github.io automl.github.io
-
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
-
- Jul 2021
-
automl.github.io automl.github.io
-
EPM
Empirical perfromance model
-
-
easychair.org easychair.org
- Jun 2021
-
-
Karel IV. Otcem vlasti, František Palacký Otcem národa
Srovnej: tatíček Masaryk, praotec Čech
-
-
www.luhovanyvincent.cz www.luhovanyvincent.cz
-
Krátké animované filmy z festivalu B16
Promítaly se filmy:
- Acid Rain
- Takové pěkné město
- M E Z E R Y
- Divoké bytosti
-
- May 2021
-
docs.python.org docs.python.org
-
special characters
Special characters:
.^$*+?{}\[]|()
-
-
automl.github.io automl.github.io
-
run_obj
Supported values:
quality
runtime
-
-
blog.czm-cvut.cz blog.czm-cvut.cz
-
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
-
-
blog.czm-cvut.cz blog.czm-cvut.cz
-
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.
Alternativa: paper-driven research
Vizte Simon Peyton Jones: How to write a great research paper: 1. Don't wait: write
-
téměř vždy je na vině student
zbytečná moralizace
-
-
www.eprover.org www.eprover.org
-
Filip Bártek and Martin SudaLearning Precedences from Simple Symbol Features
-
- Apr 2021
-
cw.fel.cvut.cz cw.fel.cvut.cz
-
Theorem3.15
Discussed in lecture on 2021-04-22
-
- Mar 2021
-
cw.fel.cvut.cz cw.fel.cvut.cz
-
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)} $$
-
- Nov 2020
-
cs231n.github.io cs231n.github.io
-
Gradient Checks
Gradient checking is only useful to debug the implementation of backpropagation: https://stackoverflow.com/questions/47506521/what-exactly-is-gradient-checking
-
-
itch.io itch.io
-
JAM THEME
Disinformation and conspiracy theories
-
- Oct 2020
-
cw.fel.cvut.cz cw.fel.cvut.cz
-
Symmetry breaking
Two propositional variables are symmetrical iff exchanging them leads to the same problem. Their identity carries no relative value.
-
-
cw.fel.cvut.cz cw.fel.cvut.cz
-
Difference logic
Why are there no propositional operations?
-
EUF
Theory of Equality and Uninterpreted Functions
-
if𝜙′/∈SAT, then return𝜙 /∈SAT
The first SAT is propositional. The second SAT is modulo T.
-
-
cw.fel.cvut.cz cw.fel.cvut.cz
-
How does the meaning of the formula change if you replace(𝑥𝑛∨𝑦𝑛∨𝑎𝑛−1)by(𝑥𝑛∨𝑎𝑛−1)∧(𝑦𝑛∨𝑎𝑛−1)?
The inequality becomes strict.
-
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\).
-
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.
-
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\).
-
-
cw.fel.cvut.cz cw.fel.cvut.czlup3.pdf5
-
How to encode typical constraints
-
hard—must be satisfied
This seems to be possible to implement with transfinite weights.
-
𝑝
Usually \(p < 0.5\).
-
Unary encoding (order encoding)
Makes expressing inequalities easy:
- \(x < i \leftrightarrow \overline{x_i}\)
- \(x \geq i \leftrightarrow x_i\)
-
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.
-
-
jazyky.fel.cvut.cz jazyky.fel.cvut.cz
-
Michael: It's up to you how much of the exercises you will do.
-
-
jazyky.fel.cvut.cz jazyky.fel.cvut.cz
-
There are few exercises in this unit and all of them are voluntary (only intended for inexperienced students).
-
-
jazyky.fel.cvut.cz jazyky.fel.cvut.cz
-
Acronyms are all right as long as they are defined explicitly first, for example:
personal protective equipment (PPE)
-
Oxford comma”
Oxford comma is useful especially when a list item contains "and", for example:
One, two and three, and four.
-
- Sep 2020
-
www.wikihow.com www.wikihow.com
-
If not, you must pick up the discard pile.
Do I get to pick the card I just flipped over as well?
-
-
jazyky.fel.cvut.cz jazyky.fel.cvut.cz
-
DO NOT use etc., i.e., or e.g.
Michael: It is ok to use these short forms in brackets.
-
hedging
What exactly is hedging? What does it look like?
-
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 [...]
-
and / or
"and / or" does not seem to be an adequate substitute for "etc." to me.
-
-
jazyky.fel.cvut.cz jazyky.fel.cvut.cz
-
Punctuation in Academic Writing
Punctuation is governed by style guides. When writing for a journal, ask them what style guide they follow.
-
-
jazyky.fel.cvut.cz jazyky.fel.cvut.cz
-
Michael prefers the participants to have their video enabled.
Homework assignments:
- Introduction (paragraph or section)
- Body (paragraph or section)
-
-
cw.fel.cvut.cz cw.fel.cvut.czlup1.pdf3
-
monotone
monotonic
-
Two formulae𝜙and𝜓are equivalent, we write𝜙≡𝜓or𝜙|=|𝜓
Cf. "equisatisfiable"
-
(𝜙1∧···∧𝜙𝑛)→(𝜓1∨···∨𝜓𝑚)
Special example: Horn clauses
-