Many-sorted logic in a learning theorem prover | Zendy

Thomas H. Kolbe | Zendy; Sabine Glesner | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Many-sorted logic in a learning theorem prover

Author(s) -

Thomas H. Kolbe,

Sabine Glesner

Publication year - 1997

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

ISBN - 3-540-63493-2

DOI - 10.1007/3540634932_5

Subject(s) - automated theorem proving , computer science , mathematical proof , gas meter prover , schematic , sort , reuse , realization (probability) , theoretical computer science , proof theory , first order logic , sequent calculus , calculus (dental) , matching (statistics) , algorithm , programming language , mathematics , information retrieval , medicine , ecology , statistics , geometry , dentistry , electronic engineering , biology , engineering

. In a learning theorem prover, formulas can be verified byreusing proofs of previously verified conjectures. Reuse proceeds by transforminga successful proof into a valid schematic formula which can beinstantiated subsequently. In this paper, we show how this reuse approachis extended to many-sorted logic: We first present the logical foundationsfor reasoning w.r.t. different sortings. Then their operational realizationis given by developing a many-sorted proof analysis calculus for...

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research