Cultural advice

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

Aboriginal and Torres Strait Islander peoples are advised that ANU Library collections may include images, names, voices, and other representations of deceased persons.

Material in the collection may contain terms, language or views that reflect the period in which the item was created and may be considered inappropriate today.

Scavenger 0.1: A Theorem Prover Based on Conflict Resolution

Simple item page
dc.contributor.authorItegulov, Daniyar
dc.contributor.authorSlaney, John
dc.contributor.authorWoltzenlogel Paleo, Bruno
dc.contributor.editorLeonardo de Moura
dc.coverage.spatialGothenburg, Sweden
dc.date.accessioned2021-09-14T03:56:04Z
dc.date.createdAugust 6-11 2017
dc.date.issued2017
dc.date.updated2020-11-23T11:05:34Z
dc.description.abstractThis paper introduces Scavenger, the first theorem prover for pure first-order logic without equality based on the new conflict resolution calculus. Conflict resolution has a restricted resolution inference rule that resembles (a first-order generalization of) unit propagation as well as a rule for assuming decision literals and a rule for deriving new clauses by (a first-order generalization of) conflict-driven clause learning.en_AU
dc.format.mimetypeapplication/pdfen_AU
dc.identifier.isbn9783319630458en_AU
dc.identifier.issn0302-9743en_AU
dc.identifier.urihttp://hdl.handle.net/1885/247857
dc.language.isoen_AUen_AU
dc.publisherSpringer International Publishing AGen_AU
dc.relation.ispartofseries26th International Conference on Automated Deduction, CADE-26 2017en_AU
dc.rights© Springer International Publishing AG 2017en_AU
dc.sourceLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)en_AU
dc.titleScavenger 0.1: A Theorem Prover Based on Conflict Resolutionen_AU
dc.typeConference paperen_AU
local.bibliographicCitation.lastpage356en_AU
local.bibliographicCitation.startpage344en_AU
local.contributor.affiliationItegulov, Daniyar, ITMO Universityen_AU
local.contributor.affiliationSlaney, John, College of Engineering and Computer Science, ANUen_AU
local.contributor.affiliationWoltzenlogel Paleo, Bruno, College of Engineering and Computer Science, ANUen_AU
local.contributor.authoruidSlaney, John, u8800435en_AU
local.contributor.authoruidWoltzenlogel Paleo, Bruno, u1002652en_AU
local.description.embargo2099-12-31
local.description.notesImported from ARIESen_AU
local.description.refereedYes
local.identifier.absfor091302 - Automation and Control Engineeringen_AU
local.identifier.ariespublicationa383154xPUB7708en_AU
local.identifier.doi10.1007/978-3-319-63046-5_21en_AU
local.identifier.essn1611-3349en_AU
local.identifier.scopusID2-s2.0-85026781419
local.publisher.urlhttps://link.springer.com/en_AU
local.type.statusPublished Versionen_AU

Downloads

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
01_Itegulov_Scavenger_0.1%3A_A_Theorem_2017.pdf
Size:
1.32 MB
Format:
Adobe Portable Document Format
Download

Collections

ANU Research Publications

DSpace software copyright © 2002-2026 LYRASIS