SRASS -- a semantic relevance axiom selection system. This paper describes the design, implementation, and testing of a system for selecting necessary axioms from a large set also containing superfluous axioms, to obtain a proof of a conjecture. The selection is determined by semantics of the axioms and conjecture, ordered heuristically by a syntactic relevance measure. The system is able to solve many problems that cannot be solved alone by the underlying conventional automated reasoning system.
Keywords for this software
References in zbMATH (referenced in 12 articles , 1 standard article )
Showing results 1 to 12 of 12.
- Furbach, Ulrich; Krämer, Teresa; Schon, Claudia: Names are not just sound and smoke: word embeddings for axiom selection (2019)
- Lopez Hernandez, Julio Cesar; Korovin, Konstantin: An abstraction-refinement framework for reasoning with large theories (2018)
- Schulz, Stephan; Sutcliffe, Geoff; Urban, Josef; Pease, Adam: Detecting inconsistencies in large first-order knowledge bases (2017)
- Kaliszyk, Cezary; Schulz, Stephan; Urban, Josef; Vyskočil, Jiří: System description: E.T. 0.1 (2015)
- Kaliszyk, Cezary; Urban, Josef: Learning-assisted theorem proving with millions of lemmas (2015)
- Kaliszyk, Cezary; Urban, Josef; Vyskočil, Jiří: Lemmatization for stronger reasoning in large theories (2015)
- Plaisted, David A.: History and prospects for first-order automated deduction (2015)
- Urban, Josef; Vyskočil, Jiří: Theorem proving in large formal mathematics as an emerging AI field (2013)
- Hoder, Kryštof; Voronkov, Andrei: Sine qua non for large theory reasoning (2011)
- Höfner, Peter; Struth, Georg; Sutcliffe, Geoff: Automated verification of refinement laws (2009)
- Sutcliffe, Geoff: The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0 (2009)
- Sutcliffe, Geoff; Puzis, Yury: SRASS -- a semantic relevance axiom selection system (2007)