In first-orderlogic induction requires an infinite number of axioms, which is not a feasible input to a computer-aided theorem prover requiring a finite input . In this work we introduce a new method, inspired by the field of axiomatictheories of truth, that allows to express schematic inductive definitions . Further we test the feasibility of the method with state-of-the-art theorem provers, comparing it to solvers’ native techniques for handling induction with their native techniques . We also compare it to the native techniques used by solvers to handle induction with a different type of inductive logic .

Author(s) : Johannes Schoisswohl, Laura Kovács

Links : PDF - Abstract

Code :

Keywords : induction - techniques - native - theorem - solvers -

Leave a Reply

Your email address will not be published. Required fields are marked *