About: Larch Prover

An Entity of Type: Thing, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

The Larch Prover, or LP for short, was an interactive theorem proving systemfor multi-sorted first-order logic. It was used at MIT and elsewhere during the 1990sto reason about designs for circuits, concurrent algorithms, hardware,and software.

Property Value
dbo:abstract
  • The Larch Prover, or LP for short, was an interactive theorem proving systemfor multi-sorted first-order logic. It was used at MIT and elsewhere during the 1990sto reason about designs for circuits, concurrent algorithms, hardware,and software. Unlike most theorem provers, which attempt to find proofs automatically forcorrectly stated conjectures, LP was intended to assist users in finding and correcting flaws inconjectures—the predominant activity in the early stages of the design process. It worked efficientlyon large problems, had many important user amenities, and could be used by relatively naïve users. (en)
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 1207000 (xsd:integer)
dbo:wikiPageLength
  • 11355 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 1062700235 (xsd:integer)
dbo:wikiPageWikiLink
dbp:wikiPageUsesTemplate
dcterms:subject
gold:hypernym
rdfs:comment
  • The Larch Prover, or LP for short, was an interactive theorem proving systemfor multi-sorted first-order logic. It was used at MIT and elsewhere during the 1990sto reason about designs for circuits, concurrent algorithms, hardware,and software. (en)
rdfs:label
  • Larch Prover (en)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
is dbo:wikiPageDisambiguates of
is dbo:wikiPageWikiLink of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License