diff --git a/README.md b/README.md index 9273e21..60b9953 100644 --- a/README.md +++ b/README.md @@ -1,18 +1,5 @@ -# vprover.github.io -The Vampire project has a [website](https://vprover.github.io)! +# Website +The website is mostly retired now and points to the wiki instead. +The hope is that this presents less of a barrier to entry for potential contributors. -The website is hosted on GitHub pages, making some use of the Jekyll templating library. -Generally stuff is obvious: copy the style of whatever is there already, it's hard to break. - -# New Members -It's nice to have you on the [team page](https://vprover.github.io/team.html)! -This is a simple process: - - put a photo of yourself in `img/`: preferably a thumbnail, square aspect works best - - add your name to `_includes/authors.html` - this allows you to have a short-form name and a hyperlink to your personal page if you like - - add a section in `team.html` with a little about you and what you're doing - use the existing people's sections as inspiration - -Push to master directly, we don't care that much. Welcome! - -# News -Add a news item by copying a file in `_posts` and updating the file name and fields accordingly. -The list of news items will be updated automatically. +If for some reason you need to fix something, it may be helpful to know that this was a 2017-era design using Jekyll and GitHub Pages. diff --git a/_includes/navigation.html b/_includes/navigation.html index 443a8c3..0e91c30 100644 --- a/_includes/navigation.html +++ b/_includes/navigation.html @@ -4,14 +4,6 @@ menu Vampire - News Download - Licence - Usage Team - Publications - History - Trophies - Projects - Workshop diff --git a/_layouts/news.html b/_layouts/news.html deleted file mode 100644 index 1cf5b29..0000000 --- a/_layouts/news.html +++ /dev/null @@ -1,18 +0,0 @@ - - - - - - - - News: {{ page.title }} - - - {% include navigation.html %} -
-
-

News: {{ page.title }}

- {{ content }} -
-
- diff --git a/_posts/2017-11-01-revamp.md b/_posts/2017-11-01-revamp.md deleted file mode 100644 index 6f4e87e..0000000 --- a/_posts/2017-11-01-revamp.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -layout: news -title: "Website Revamp" -date: 2017-11-01 ---- - -The Vampire website is being re-vamped. diff --git a/_posts/2017-12-05-vampire-source-available.md b/_posts/2017-12-05-vampire-source-available.md deleted file mode 100644 index fbb6bbf..0000000 --- a/_posts/2017-12-05-vampire-source-available.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -layout: news -title: "Vampire Source Available" -date: 2017-12-05 ---- - -The Vampire source is now available via our [GitHub repository](https://github.com/vprover/vampire). diff --git a/_posts/2017-12-10-vampire-mailing-list.md b/_posts/2017-12-10-vampire-mailing-list.md deleted file mode 100644 index 9fc710c..0000000 --- a/_posts/2017-12-10-vampire-mailing-list.md +++ /dev/null @@ -1,7 +0,0 @@ ---- -layout: news -title: "Vampire Mailing List" -date: 2017-12-10 ---- - -We have set up a new mailing list to allow us to contact those interested in Vampire. You can sign up here. Traffic will be very low (new majory releases, publiciations, competition successes etc). diff --git a/_sass/pubs.scss b/_sass/pubs.scss deleted file mode 100644 index 6ffc40a..0000000 --- a/_sass/pubs.scss +++ /dev/null @@ -1,55 +0,0 @@ -ol.pubs li.year h2 -{ - text-align: left; -} - -ol.pubs -{ - counter-reset: ref; -} - -ol.pubs > li.year -{ - list-style: none; - margin: 0; -} - -ol.pubs > li.paper -{ - list-style: none; - counter-increment: ref; - margin: 0; -} - -ol.pubs > li.paper:before -{ - content: "[" counter(ref, decimal-leading-zero) "]"; -} - -ol.pubs ul -{ - display: inline; -} - -ol.pubs ul li -{ - margin: 0; - padding: 0; - display: inline; - list-style: none; -} - -ol.pubs ul li a:after -{ - content: ","; -} - -ol.pubs ul li:last-child a:after -{ - content: "."; -} - -ol.pubs cite:after -{ - content: "."; -} diff --git a/bin/vampire4.2.2 b/bin/vampire4.2.2 deleted file mode 100755 index f6aadd9..0000000 Binary files a/bin/vampire4.2.2 and /dev/null differ diff --git a/bin/vampire4.2.2_noz3 b/bin/vampire4.2.2_noz3 deleted file mode 100755 index eec37aa..0000000 Binary files a/bin/vampire4.2.2_noz3 and /dev/null differ diff --git a/bin/vampire4.5_precasc b/bin/vampire4.5_precasc deleted file mode 100755 index 297f60b..0000000 Binary files a/bin/vampire4.5_precasc and /dev/null differ diff --git a/bin/vampire4.5_precasc_thf b/bin/vampire4.5_precasc_thf deleted file mode 100644 index 3166ddf..0000000 Binary files a/bin/vampire4.5_precasc_thf and /dev/null differ diff --git a/bin/vampire_rel_static_release_v4.4 b/bin/vampire_rel_static_release_v4.4 deleted file mode 100755 index 0135908..0000000 Binary files a/bin/vampire_rel_static_release_v4.4 and /dev/null differ diff --git a/bin/vampire_z3_rel_static_release_v4.4 b/bin/vampire_z3_rel_static_release_v4.4 deleted file mode 100755 index 8223668..0000000 Binary files a/bin/vampire_z3_rel_static_release_v4.4 and /dev/null differ diff --git a/history.html b/history.html deleted file mode 100644 index aa69783..0000000 --- a/history.html +++ /dev/null @@ -1,55 +0,0 @@ ---- -title: History -layout: default ---- -{% include authors.html %} - -

-Vampire had several predecessors implemented by {{ voronkov }} in the International Laboratory of Intelligent Systems in Novosibirsk from 1990. -The first predecessor that was actually able to prove something appeared in 1989 and called Drakosha. -It has been implemented in LISP. -

- -
- Andrei Voronkov -
Voronkov, just a few years ago
-
- -

-There have been three major incarnations of Vampire itself, all -implemented in C++. -

- -
    -
  1. -The first incarnation was born in Uppsala University in 1994 after {{ voronkov }}'s visit to the Bull Research Lab. -This implementation was used for the first experiments with code trees and a pre-CASC competition with the SETHEO theorem prover in Munich. -
  2. -The second re-incarnation appeared in Uppsala University and then wandered to the University of Manchester. -It has been developed from the first incarnation (that was eventually completely rewritten) by {{ voronkov }} and Alexandre Riazanov in 1998. -From 2005 it has been developed and maintained by {{ voronkov }}. -This incarnation has been winning the CASC competitions since 1999. -
  3. -The work on the third re-incarnation of Vampire started in 2008. -It has been developed by {{ voronkov }} and {{ hoder }}. -This version used some code and algorithms for preprocessing from the second re-incarnation but re-implemented the resolution and superposition engine from scratch. -The version used in CASC 2009 was actually a combination of the second and the third reincarnation glued by Perl scripts called Dracula and Drakosha. -
  4. Since {{ hoder }} decided to leave academia and help Larry Page and Sergey Brin to make more money, Vampire is waking up for its fourth reincarnation. -Several people are working on it. -A considerable amount of code was contributed by {{ kovacs }}, mainly in Vampire's program analysis, interpolation and symbol elimination parts. -
- -
- Alexandre Riazanov -
Alexandre Riazanov
-
- -

-From 2014, the current team took over the active development of Vampire. -Whilst the current version is labelled as the fourth reincarnation, much of the core still consists of code written by {{ hoder }} in the third incarnation. -

- -
- Krystof Hoder -
Krystof Hoder
-
diff --git a/index.html b/index.html index 6e464d7..0dd91a4 100644 --- a/index.html +++ b/index.html @@ -4,30 +4,23 @@ ---

-Automatic theorem proving has a number of important applications, such as software verification, hardware verification, - hardware design, knowledge representation and reasoning, the Semantic Web, algebra, and proving theorems in mathematics. -Over 50 years of research in theorem proving have resulted in one of the most advanced and elegant theories in - computer science. -This area is an ideal target for scientific engineering: implementation techniques have to be developed to realise - an advanced theory in practically valuable tools. +Automatic theorem proving has a number of important applications, such as software verification, hardware verification, hardware design, knowledge representation and reasoning, the Semantic Web, algebra, and proving theorems in mathematics. +Over 50 years of research in theorem proving have resulted in one of the most advanced and elegant theories in computer science. +This area is an ideal target for scientific engineering: implementation techniques have to be developed to realise an advanced theory in practically valuable tools.

-Vampire is a theorem prover, that is, a system able to prove theorems — although now it can do much more! -Its main focus is in proving theorems in first-order logic but it can also prove non-theorems and build finite models, as well as reasoning in combinations of theories, such as arithmetic, arrays, and datatypes, and with higher-order logic. -The development of Vampire began in 1994 and has survived a number of rewritings (see history). -

- -

NEW LICENCE! We are very pleased to announce that Vampire is now available under a BSD 3-Clause licence, allowing (free) industrial and academic usage. - It would be great to hear from you if you are making use of this new licence within your work. Please join our very low-traffic mailing list for updates. -You may also want to want to use the GitHub Issues page for questions or issues. +Vampire is a theorem prover, that is, a system able to prove theorems — although now it can do much more! +Its main focus is in proving theorems in first-order logic but it can also prove non-theorems and build finite models, as well as reasoning in combinations of theories, such as arithmetic, arrays, and datatypes, and with higher-order logic. +The development of Vampire began in 1994 and has survived a number of rewrites (see history). +Vampire is available under a modified BSD 3-clause licence (see the LICENCE), allowing (free) industrial and academic use.

Features