Journal of Automated Reasoning

Automated discovery of geometric theorems has attracted considerable attention from the research community. In this paper, a new method is proposed to discover geometric theorems automatically. This method first generates vector equations based on ...

The development of domain-independent planners within the AI planning community is leading to “off-the-shelf” technology that can be used in a wide range of applications. Moreover, it allows a modular approach—in which planners and domain ...

Leo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The prover may cooperate with ...

Intensional sets, i.e., sets given by a property rather than by enumerating elements, are widely recognized as a key feature to describe complex problems (see, e.g., specification languages such as B and Z). Notwithstanding, very few tools exist ...${\mathcal{}}_{\mathcal{}}$$\mathcal{}$$\mathcal{}$${\mathcal{}}_{\mathcal{}}$$\mathcal{}$$$