Limited resource strategy in resolution theorem proving
type: Item
instance of: scholarly article
title: Limited resource strategy in resolution theorem proving
zbMATH Open document ID: 1023.68089
DOI: 10.1016/S0747-7171(03)00040-3
author: Alexandre Riazanov
author: Andrei Voronkov
published in: Journal of Symbolic Computation
publication date: 2003-08-25T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 1970572
zbMATH Keywords: automated theorem proving
zbMATH Keywords: limited resource strategy
zbMATH Keywords: resolution
zbMATH Keywords: OTTER saturation algorithm
describes a project that uses: VAMPIRE
describes a project that uses: OTTER
describes a project that uses: DISCOUNT
describes a project that uses: Waldmeister
describes a project that uses: Bliksem
describes a project that uses: E-SETHEO
describes a project that uses: SETHEO
describes a project that uses: SPASS
MaRDI profile type: Publication
cites work: Q4524770
cites work: Logic programming and automated reasoning. International conference, LPAR `92, St. Peterburg, Russia, July 15--20, 1992. Proceedings
cites work: Q4539610
cites work: Q4539622
cites work: Q4539621
cites work: Term indexing
cites work: The CADE-16 ATP system competition
description: scientific article; zbMATH DE number 1970572