The following pages link to Cezary Kaliszyk (Q286799):
Displaying 47 items.
- MizAR 40 for Mizar 40 (Q286800) (← links)
- A learning-based fact selector for Isabelle/HOL (Q331617) (← links)
- Learning-assisted theorem proving with millions of lemmas (Q485842) (← links)
- JEFL: joint embedding of formal proof libraries (Q831932) (← links)
- Aligning concepts across proof assistant libraries (Q1640642) (← links)
- Towards a unified ordering for superposition-based automated reasoning (Q1662244) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Automating formalization by statistical and semantic parsing of mathematics (Q1687711) (← links)
- Towards formal foundations for game theory (Q1791194) (← links)
- Concrete semantics with Coq and CoqHammer (Q1798946) (← links)
- Isabelle import infrastructure for the Mizar Mathematical Library (Q1798961) (← links)
- First experiments with neural translation of informal to formal mathematics (Q1798975) (← links)
- HOL(y)Hammer: online ATP service for HOL Light (Q2018657) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
- Machine learning guidance for connection tableaux (Q2031418) (← links)
- Lash 1.0 (system description) (Q2104521) (← links)
- Online machine learning techniques for Coq: a comparison (Q2128797) (← links)
- Towards finding longer proofs (Q2142073) (← links)
- Certification of nonclausal connection tableaux proofs (Q2180504) (← links)
- Mac Lane's comparison theorem for the Kleisli construction formalized in Coq (Q2209259) (← links)
- Relaxed weighted path order in theorem proving (Q2209265) (← links)
- A survey of languages for formalizing mathematics (Q2219386) (← links)
- GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
- Semantics of Mizar as an Isabelle object logic (Q2323445) (← links)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) (Q2351415) (← links)
- Erratum to: ``Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)'' (Q2352503) (← links)
- Presentation and manipulation of Mizar properties in an Isabelle object logic (Q2364678) (← links)
- Classification of alignments between concepts of formal mathematical systems (Q2364703) (← links)
- Monte Carlo tableau proof search (Q2405274) (← links)
- What’s in a Theorem Name? (Q2829279) (← links)
- Automated Reasoning Service for HOL Light (Q2843009) (← links)
- Formal Mathematics on Display: A Wiki for Flyspeck (Q2843012) (← links)
- Algebraic Analysis of Huzita’s Origami Operations and Their Extensions (Q2849512) (← links)
- Web Interfaces for Proof Assistants (Q2867935) (← links)
- Lemma Mining over HOL Light (Q2870150) (← links)
- Learning to Parse on Aligned Corpora (Rough Diamond) (Q2945635) (← links)
- Random Forests for Premise Selection (Q2964471) (← links)
- Lemmatization for Stronger Reasoning in Large Theories (Q2964472) (← links)
- Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem (Q3100205) (← links)
- (Q3184782) (← links)
- Deep Network Guided Proof Search (Q4645728) (← links)
- TacticToe: Learning to Reason with HOL4 Tactics (Q4645730) (← links)
- A study of continuous vector representations for theorem proving (Q5019287) (← links)
- Hammering towards QED (Q5195271) (← links)
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. (Q5875415) (← links)
- Declarative Proof Translation (Short Paper) (Q5875449) (← links)
- Combining higher-order logic with set theory formalizations (Q6161232) (← links)
