leanCoP: lean connection-based theorem proving

摘要

The connection calculus (Bibel, 1983, 1987, 1993), the connection tableau calculus (Letz et al., 1994) and the similar model elimination calculus (Loveland, 1968) are popular and successful proof procedures because of their goal-oriented search strategy. Several proof systems based on one of these approaches have been developed, e.g. KoMET (Bibel et al., 1994), SETHEO (Letz et al., 1992; Moser et al., 1997) and METEOR (Astrachan and Loveland, 1991) to name but a few. All these systems have shown to be an appropriate basis to automate formal reasoning in classical first-order logic.