This HTML5 document contains 31 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
dbohttp://dbpedia.org/ontology/
foafhttp://xmlns.com/foaf/0.1/
n10https://global.dbpedia.org/id/
dbthttp://dbpedia.org/resource/Template:
rdfshttp://www.w3.org/2000/01/rdf-schema#
freebasehttp://rdf.freebase.com/ns/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
owlhttp://www.w3.org/2002/07/owl#
wikipedia-enhttp://en.wikipedia.org/wiki/
dbphttp://dbpedia.org/property/
dbchttp://dbpedia.org/resource/Category:
provhttp://www.w3.org/ns/prov#
xsdhhttp://www.w3.org/2001/XMLSchema#
wikidatahttp://www.wikidata.org/entity/
dbrhttp://dbpedia.org/resource/

Statements

Subject Item
dbr:Proof_compression
dbo:wikiPageWikiLink
dbr:Resolution_proof_reduction_via_local_context_rewriting
Subject Item
dbr:Resolution_proof_reduction_via_local_context_rewriting
rdfs:label
Resolution proof reduction via local context rewriting
rdfs:comment
In proof theory, an area of mathematical logic, resolution proof reduction via local context rewriting is a technique for resolution proof reduction via local context rewriting. This proof compression method was presented as an algorithm named ReduceAndReconstruct, that operates as a post-processing of resolution proofs. ReduceAndReconstruct is based on a set of local proof rewriting rules that transform a subproof into an equivalent or stronger one. Each rule is defined to match a specific context. The first five rules were introduced in an earlier paper. In addition:
dcterms:subject
dbc:Articles_with_example_pseudocode dbc:Proof_theory
dbo:wikiPageID
35307890
dbo:wikiPageRevisionID
942706921
dbo:wikiPageWikiLink
dbr:Heuristic dbr:Proof_compression dbr:Rewriting dbc:Proof_theory dbr:Topological_ordering dbr:Mathematical_logic dbr:Directed_acyclic_graph dbr:RecyclePivots dbr:Proof_theory dbc:Articles_with_example_pseudocode dbr:Resolution_(logic) dbr:Resolution_graph
owl:sameAs
n10:4tXTF freebase:m.0j7k59z wikidata:Q7315700
dbp:wikiPageUsesTemplate
dbt:EquationNote dbt:EquationRef dbt:NumBlk dbt:Reflist
dbo:abstract
In proof theory, an area of mathematical logic, resolution proof reduction via local context rewriting is a technique for resolution proof reduction via local context rewriting. This proof compression method was presented as an algorithm named ReduceAndReconstruct, that operates as a post-processing of resolution proofs. ReduceAndReconstruct is based on a set of local proof rewriting rules that transform a subproof into an equivalent or stronger one. Each rule is defined to match a specific context. A context involves two pivots ( and ) and five clauses . The structure of a context is shown in. Note that this implies that is contained in and (with opposite polarity) and is contained in and (also with opposite polarity). The table below shows the rewriting rules proposed by Simone et al.. The idea of the algorithm is to reduce proof size by opportunistically applying these rules. The first five rules were introduced in an earlier paper. In addition: * Rule A2 does not perform any reduction on its own. However, it is still useful, because of its "shuffling" effect that can create new opportunities for applying the other rules; * Rule A1 is not used in practice, because it may increase proof size; * Rules B1, B2, B2' and B3 are directly responsible for the reduction, as they produce a transformed root clause stronger than the original one; * The application of a B rule may lead to an illegal proof (see the example below), as some literals missing in the transformed root clause may be involved in another resolution step along the path to the proof root. Therefore, the algorithm also has to "reconstruct" a legal proof when this happen. The following example shows a situation where the proof becomes illegal after the application of B2' rule: Applying rule B2' to the highlighted context: The proof is now illegal because the literal is missing from the transformed root clause. To reconstruct the proof, one can remove together with the last resolution step (that is now redundant). The final result is the following legal (and stronger) proof: A further reduction of this proof by applying rule A2 to create a new opportunity to apply rule B2'. There are usually a huge number of contexts where rule A2 may be applied, so an exhaustive approach is not feasible in general. One proposal is to execute ReduceAndReconstruct as a loop with two termination criteria: number of iterations and a timeout (what is reached first). The pseudocode below shows this. 1 function ReduceAndReconstruct( /* a proof */, timelimit, maxIterations): 2 for i = 1 to maxIterations do 3 ReduceAndReconstructLoop; 4 if time > timelimit then // timeout 5 break; 6 end for 7 end function ReduceAndReconstruct uses the function ReduceAndReconstructLoop, which is specified below. The first part of the algorithm does a topological ordering of the (considering that edges goes from antecedentes to resolvents). This is done to ensure that each node is visited after its antecedents (this way, broken resolution steps are always found and fixed). 1 function ReduceAndReconstructLoop( /* a proof */): 2 TS = TopologicalSorting; 3 for each node in TS 4 if is not a leaf 5 if and then 6 = Resolution; 7 Determine left context of , if any; 8 Determine right context of , if any; 9 Heuristically choose one context (if any) and apply the corresponding rule;10 else if and then11 Substitute with ;12 else if and then13 Substitute with ;14 else if and then15 Heuristically choose an antecedent or ;16 Substitute with or ;17 end for18 end function If the input proof is not a tree (in general, resolution graphs are directed acyclic graphs), then the clause of a context may be involved in more than one resolution step. In this case, to ensure that an application of a rewriting rule is not going to interfere with other resolution steps, a safe solution is to create a copy of the node represented by clause . This solution increases proof size and some caution is needed when doing this. The heuristic for rule selection is important to achieve a good compression performance. Simone et al. use the following order of preference for the rules (if applicable to the given context): B2 > B3 > { B2', B1 } > A1' > A2 (X > Y means that X is preferred over Y). Experiments have shown that ReduceAndReconstruct alone has a worse compression/time ratio than the algorithm . However, while RecyclePivots can be applied only once to a proof, ReduceAndReconstruct may be applied multiple times to produce a better compression. An attempt to combine ReduceAndReconstruct and RecyclePivots algorithms has led to good results.
prov:wasDerivedFrom
wikipedia-en:Resolution_proof_reduction_via_local_context_rewriting?oldid=942706921&ns=0
dbo:wikiPageLength
10543
foaf:isPrimaryTopicOf
wikipedia-en:Resolution_proof_reduction_via_local_context_rewriting
Subject Item
wikipedia-en:Resolution_proof_reduction_via_local_context_rewriting
foaf:primaryTopic
dbr:Resolution_proof_reduction_via_local_context_rewriting