• Michael Kohlhase, A Mechanization of Sorted Higher-Order Logic Based on the Resolution Principle.
    The usage of sorts in first-order automated deduction has brought greater conciseness of representation and a considerable gain in efficiency by reducing the search spaces involved. This suggests that sort information can be employed in higher-order theorem proving with similar results.
    No categories
    In my reading list   |  Discuss this article  |  Edit  |  Categorize  |  
     
    My bibliography  |
     
    Export citation | Scholar
    1 download  |  Added to index:2010-02-06  |  Mark as duplicate |  Delete from index