@inproceedings{489f6a8b12b348ac82a92083c444bdf9,
title = "A focusing inverse method theorem prover for first-order linear logic",
abstract = "We present the theory and implementation of a theorem prover for first-order intuitionistic linear logic based on the inverse method. The central proof-theoretic insights underlying the prover concern resource management and focused derivations, both of which arc traditionally understood in the domain of backward reasoning systems such as logic programming. We illustrate how resource management, focusing, and other intrinsic properties of linear connectives affect the basic forward operations of rule application, contraction, and forward subsumption. We also present some preliminary experimental results obtained with our implementation.",
author = "Kaustuv Chaudhuri and Frank Pfenning",
year = "2005",
month = jan,
day = "1",
doi = "10.1007/11532231\_6",
language = "English",
isbn = "3540280057",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "69--83",
booktitle = "Automated Deduction - CADE-20 - 20th International Conference on Automated Deduction, Proceedings",
note = "20th International Conference on Automated Deduction, CADE-20 ; Conference date: 22-07-2005 Through 27-07-2005",
}