Open AccessSTRIP: Structural Sharing for Efficient Proof-Search
Author(s) -
Dominique Larchey-Wendling,
Domingo Mery,
Didier Galmiche
Publication year - 2001
Publication title -
lecture notes in computer science
Language(s) - English
Resource type - Book series
SCImago Journal Rank - 0.249
H-Index - 400
eISSN - 1611-3349
pISSN - 0302-9743
DOI - 10.1007/3-540-45744-5_58
Subject(s) - automated theorem proving , computer science , gas meter prover , proof theory , proof complexity , propositional calculus , structural proof theory , proof assistant , theoretical computer science , algorithm , calculus (dental) , discrete mathematics , programming language , mathematics , mathematical proof , geometry , medicine , dentistry
The STRIP system is a theorem prover for intuitionistic propositional logic with two main characteristics: it deals with the duplication of formulae during proof-search from a fine and explicit management of formulae (as resources) based on a structural sharing and it builds, for a given formula, either a proof or a countermodel.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom