Stream Matryoshka

• Full HOL sup
• hello
• Calculus proposal for FOL with interpreted Booleans
• CADE 2019 papers
• Bools
• motivational_story.jpg
• Positive/Negative simplify reflect + AC reasoning
• Unification modulo vs Cases
• HOunif reeval
• Evatar (avatar-lite)
• eligible literals
• Problem SEU909^5
• Matryoshka web site
• FluidCases
• Moving the Matryoshka git repo
• Saturation framework for FOL with Booleans?
• Nasty (performance) bug
• Benchmark sets
• Vampire's new HO Superposition calculus
• Coauthorship HOSUP/FO with interpreted bool
• BoolSimp
• Injectivity
• LPAR 2021
• Calculi Names
• Delaying open terms
• Superposition with Lambdas
• Lean together 2021
• Clauses as terms with 1ˢᵗ-class bools
• Problem SEU868^5
• Superposition with lambdas
• opam switch 4.10.0(+flambda)
• SYO544^4
• Embedding Path Order
• Paper draft - Verifying Saturation Provers Modularly
• Non-syntactic heuristics
• Standard HOL
• Soundness theorems
• DupSup and completeness
• Terminology question
• Lazy clausification
• Superposition for lambda-free HOL
• SEU929^5
• welcome
• Combinators vs Lambdas
• SEV244^5
• Santa Clause
• GRUNGE paper
• Superposition and EqFact conditions
• Saturation framework
• Connectedness criterion
• Defintion of the TRS with booleans
• Problem SEU794^2
• Git repositories
• New AVATAR issue
• curious about this set-based ITP
• Superposition for FOL with interpreted Booleans
• Description of PruneArg
• Name for simp rule
• δElim and basic superposition
• Enumeration of bool functions
• (cont): long lived academic content
• VU people
• Lazy clausification for FOOL
• Testing
• evil axioms
• Lambda-free superposition
• Profiler
• Skolemization and saturation framework
• ExtInf
• HOSup (and BoolSup)
• System description
• smt-proofs-equality-order