Translating SUMO-K to Higher-Order Set Theory
From MaRDI portal
Publication:6496634
DOI10.1007/978-3-031-43369-6_14MaRDI QIDQ6496634
Josef Urban, Adam Pease, Chad Edward Brown
Publication date: 3 May 2024
Cites Work
- Unnamed Item
- Automating formalization by statistical and semantic parsing of mathematics
- First experiments with neural translation of informal to formal mathematics
- The higher-order prover Leo-III
- Lash 1.0 (system description)
- A tale of two set theories
- ENIGMA-NG: efficient neural and gradient-boosted inference guidance for \(\mathrm{E}\)
- ENIGMA: efficient learning-based inference guiding machine
- Detecting inconsistencies in large first-order knowledge bases
- The TPTP Typed First-Order Form with Arithmetic
- Learning to Parse on Aligned Corpora (Rough Diamond)
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- Large theory reasoning with SUMO at CASC
- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (System Description)
- Developing Corpus-Based Translation Methods between Informal and Formal Mathematics: Project Description
- Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
- Hammering Mizar by Learning Clause Guidance (Short Paper).
- Making higher-order superposition work
This page was built for publication: Translating SUMO-K to Higher-Order Set Theory
