System description: E-KRHyper. The E-KRHyper system is a model generator and theorem prover for first-order logic with equality. It implements the new E-hyper tableau calculus, which integrates a superposition-based handling of equality into the hyper tableau calculus. E-KRHyper extends our previous KRHyper system, which has been used in a number of applications in the field of knowledge representation. In contrast to most first order theorem provers, it supports features important for such applications, for example queries with predicate extensions as answers, handling of large sets of uniformly structured input facts, arithmetic evaluation and stratified negation as failure. It is our goal to extend the range of application possibilities of KRHyper by adding equality reasoning.
Keywords for this software
References in zbMATH (referenced in 12 articles , 2 standard articles )
Showing results 1 to 12 of 12.
- Baumgartner, Peter; Schmidt, Renate A.: Blocking and other enhancements for bottom-up model generation methods (2020)
- Claudia Schon, Sophie Siebert, Frieder Stolzenburg: Using ConceptNet to Teach Common Sense to an Automated Theorem Prover (2019) arXiv
- Furbach, Ulrich; Krämer, Teresa; Schon, Claudia: Names are not just sound and smoke: word embeddings for axiom selection (2019)
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: inference system and completeness (2017)
- Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
- Bonacina, Maria Paola; Furbach, Ulrich; Sofronie-Stokkermans, Viorica: On first-order model-based reasoning (2015)
- Furbach, Ulrich; Schon, Claudia: Deontic logic for human reasoning (2015)
- Bender, Markus; Pelzer, Björn; Schon, Claudia: System description: E-KRhyper 1.4. Extensions for unique names and description logic (2013)
- Furbach, Ulrich; Schon, Claudia: Semantically guided evolution of (\mathcalSHI) ABoxes (2013)
- Baumgartner, Peter; Pelzer, Björn; Tinelli, Cesare: Model evolution with equality -- revised and implemented (2012)
- Furbach, Ulrich; Glöckner, Ingo; Helbig, Hermann; Pelzer, Björn: Logic-based question answering (2010) ioport
- Pelzer, Björn; Wernhard, Christoph: System description: E-KRHyper (2007)