Saturday, April 20, 2019

How to Build & Run Vampire ATP in Cygwin

Vampire is an Automated Theorem Prover.  It was apparently developed on Linux, but it can be run on Windows using Cygwin, which provides the build tools, software packages and operating system services that Vampire depends on.  Here are some instructions for building and running Vampire in 64-bit Windows 10.  A note on building Vampire with Cygwin can be found on Vampire's GitHub page, here.

Install Cygwin:

  1. Install Cygwin and its default packages.
  2. Install these Cygwin packages:
    • cygrunsrv
    • gcc-core
    • gcc-g++
    • make
    • zlib
    • zlib-devel
    • zlib-devel
    • zlib0
  3. Move C:\cygwin64\bin to the front of the %PATH% environment variable.

Install Git Command-Line Tools

  1. Install the Git command-line tools.  An installer can be downloaded from https://git-scm.com/download/win.

Install the Z3 Theorem Prover

  1. Download a Win64 release of Z3 from https://github.com/Z3Prover/z3/releases.
  2. Make z3.dll available from PATH, either by putting z3.dll from this release in some folder that is in PATH, or by adding the Z3 "bin" folder to PATH.

Build Vampire

  1. Pull Vampire's Git repository from GitHub (https://github.com/vprover/vampire).
  2. In Vampire's Makefile, add "-D_GNU_SOURCE" to CXXFLAGS and CCFLAGS.
  3. Change all instances of "exit(0);" in the source code to "_Exit(0);".  This is needed to prevent the child processes forked by the main Vampire process from calling the main process' atexit handlers.
  4. Create a folder named "include" in the Vampire repository's main folder.
  5. Copy the contents of the Z3 "bin" folder to that "include" folder.
  6. Compile and link vampire by issuing the command "make vampire_z3_rel" from a command prompt.

Start the Cygwin Windows Service

  1. Start Cygwin's bash shell.
  2. From the bash command prompt, issue the command "cygserver-config" to configure the Cygwin Windows service.
  3. In Windows, right-click "This PC", select "Manage", then select "Services and Applications, then select "Services", then start the "CYGWIN cygserver" service.

 Run Vampire

  1. Run Vampire from a command prompt.  For example:
    vampire_z3_rel_master_4055 --mode casc -t 300 "Problems\SET\SET159-6.p"
  2. Vampire may not succeed in deleting the semaphores that it creates in the Cygwin server.  To delete them, issue the command "ipcs -s | grep '^s\\s' | cut -d' ' -f3|xargs -n 1 ipcrm -s" from a command prompt.  Alternatively, add a call to system() at the end of Vampire's main function that issues this command.

        Sunday, May 06, 2018

        Historical and Cultural Context for the New Testament

        Years ago, I read an article about how some Japanese toilets have special built-in features, including electric seat warmers.  I thought this was weird.  I would not want to sit on a warmed toilet seat and I didn't understand why someon else would.  I couldn't explain it further than thinking to myself that different people feel differently about different things.  Many years later, I talked to friend who had returned to the U.S. after spending some months living in Japan.  He told me that the Japanese did not heat their entire homes.  In cold seasons, they would heat the space they were staying in, or just their beds at night.  After learning that, I was able figure out for myself why a Japanese person would want a seat warmer on their toilet.  In an American, climate-controlled house, a room-temperature toilet seat is about 70 degrees Fahrenheit.  A warmed toilet seat would be unpleasantly warm; to me it would feel like someone had just been sitting on the seat.  Though I fully accept that other people use the same toilet seats as me, I don't like to be reminded of the fact.  Now, what if room temperature is 50 degrees?  Suddenly, the toilet seat warmer made sense to me.

        So what does this have to do with the Bible?  It shows that context matters.  If you want to understand why people in other cultures do what they do, it helps a lot to understand their circumstances.  This goes doubly when people aren't just separated from you by distance and borders, but also by long stretches of time.  I like to think the Bible mostly speaks for itself, but really there's a lot in it that might not make sense to a modern reader.  In recent years, I've got into reading about the historical and cultural context of the Bible, expecially the New Testament.  It's been so helpful to me in making sense of difficult parts that I think everyone who seriously wants to understand the Bible should do it.  The following are some books that I recommend to anyone who wants to learn about the historical and cultural context of the New Testament.  None are very long and I don't think any require much background apart from the Bible itself and some general knowledge of the Roman empire.

        Poet & Peasant and Through Peasant Eyes: A Literary-Cultural Approach to the Parables in Luke  by Kenneth E. Bailey

        You may have heard in a sermon that it's important that the father of the Prodigal Son runs to his son when he returns because in traditional Middle Eastern cultures, it's undignified for a grown man to run.  Ok, maybe not, but in my experience those kinds of facts appear in sermons every once in a while.  If you had, you might wonder where that bit of information from came from.   The answer is the late Kenneth E. Bailey.  Bailey wrote several books that interpret parts of the Bible using his knowledge of Middle Eastern culture and customs as well as his knowledge of ancient Middle Eastern Bible translators and commentators.  Poet & Peasant and Through Peasant Eyes are two of the earliest of these books, combined into one volume.  In them, he explains how Jesus' contemporaries would likely have understood several of Jesus' parables.  Not only that, he analyzes the structure of the parables, showing that their sentences are arranged deliberately in known rhetorical forms.  I love these books and consequently I love Kenneth Bailey.  There is so much insight to be had from them. 

        Jerusalem in the Time of Jesus by Joachim Jeremias

        A wide-ranging book about... Jerusalem in the time of Jesus.  Lots of information about the size, structure and economy of Jerusalem and other interesting things like trades and Jewish marriage customs.  Perhaps most useful for understanding the New Testament are the sections about Jewish religious groups.  They explain who the Pharisees and the Sadducees were, and who those "scribes" were that Jesus was arguing with in the Gospels.

        Josephus: Thrones of Blood

        This is an abridgement and paraphrase of two of Josephus' books: The Antiquities of the Jews and The Jewish War.  In these books, Josephus writes for a Roman audience, giving an account of the history of the Jewish nation from the times of the Herods to the destruction of Jerusalem in 70 A.D.  The modern language of this paraphrase makes it easier to read than the older English translations, and it's not a long book.  It's good for understanding the political climate that Jesus and his disciples lived in.

        Slaves, Citizens, Sons: Legal Metaphors in the Epistles by Francis Lyall

        In this book, Lyall explains Roman, Greek and Hebrew law pertaining to slavery, citizenship, sonship, inheritance and adoption.  Dry stuff?  No, because it's useful for understanding what Paul means when he writes about being adopted into God's family, being "sons of God", being a "bondservant of Christ", etc.  It's also interesting to see how some things that so many modern people take for granted, like the fact that laws apply to all individuals in a society, just weren't so in the ancient world, especially Rome.  In Roman law, only free men (usually heads of households) were subject to law.  Everyone else -- women, children, slaves and unemancipated sons -- were considered to be property and therefore considered to be "objects" as far as laws were concerned.

        The Old Testament Apocrypha

        For most of my life, I never read the Apocrypha or thought much about them.  But then I read N. T. Wright's series, "Christian Origins and the Question of God".  In these books, he references them so often that I had to read them to know what he was talking about.  Most were boring to me.  2 Esdras is strange.  I found Ben Sirach's proverbs to be interesting; some are good, but others are worldly and self-interested.  Some are even contrary to what Jesus taught, which reinforces my Protestant belief that it should be canonical.  Even so, these books were read by Jesus' contemporaries and are likely to represent their worldview.  Also, they fill in some of the gap between Old Testament and New Testament history.

        Saturday, March 31, 2018

        Improvements to somerby.net/mack/logic

         After a spate of good input from commenters, I've improved somerby.net/mack/logic in several ways:
        • Instead of showing just one counterexample, clicking the "Counterexample" button more than once causes the application to cycle through different counterexamples for the current statement.
        • There is a new button: the "Example" button, which is the opposite of the "Counterexample" button.
        • Propositions (nullary predicates) can now be lower-case letters as well as upper-case letters.
        • There is now a "therefore" operator -- ',' -- apostrophe comma apostrophe, for representing logical arguments.

        Sunday, October 15, 2017

        The Video Fuzz: a Fuzz Pedal Based on the S9014 Transistor


        I built a fuzz pedal for my guitar using parts from an old, off-brand Nintendo accessory called the "Video Shooter" and a broken Fender Frontman amplifier.  The pedal is based on the Bazz Fuss, which is a simple fuzz circuit that is easy to modify.  I wanted to use parts from the Nintendo accessory as much as possible, so I designed the circuit around the accessory's enclosure and the S9014 transistors I found inside.  One S9014 did not put out enough gain to work as a guitar effect, so, after reading this forum thread, I joined two transistors into what is called a "Darlington transistor".  The happy result was sufficient gain and a very well-behaved fuzz pedal.  Unlike some other Bazz Fuss derivatives I have encountered, it doesn't fizzle or sputter when connected to a guitar with high-impedance pickups and or when I roll off the volume on the guitar.  Its gain is moderate.  I call it the "Video Fuzz" in honor of the NES accessory

        Since it's so well-behaved, I'm sharing the schematic here in case anyone wants a good starting point for their own fuzzy experimentations:

        Video Shooter Fuzz Schematic
        If you compare the circuit to the original Bazz Fuss, you'll notice I added a resistor in front of the pot going to the output.  I did this because the output is well above unity gain even with 47k Ohms resistance; I'd never want to use the full range of a 100k Ohm pot.  I added a 2.2k Ohm resistor at at the collector of the transistor to set the fuzz to a level that sounded good to me.  I could have put a pot at the collector to have a two-knob fuzz, but instead I opted to make a one-knob fuzz and control the fuzz level with my guitar's volume knob.  For the switch and jack wiring, I used the wiring shown second to last in DIYStrat: Wiring a Stomp Box. Here is the finished pedal:


        This is the fuzz circuit by itself, minus the 50k Ohm pot:

        Hand-Soldered, Point-to-Point Wiring!
        I won't show you rest of the insides; you've seen enough of the sausage being made.

        And here are some sound clips: (1), (2).  Interestingly, when I was first wiring a Bazz Fuss circuit, I connected the collector and the pot to the negative end of a battery but not to ground and the resulting circuit made no distortion and behaved like a buffer. 


        Monday, September 04, 2017

        Alternative Hexadecimal Digits: Published

        Valdis and I wrote up our final version of the hexadecimal digits in the form of a proposal and got it published in the IJCSET.  See here.  The proposal includes descriptions and assessments of various other proposed sets of hexadecimal digits.  Unfortunately, we missed a good set called Birkana that are rune-like symbols.

        In case anyone wants to see our digits used for practical purposes, I made a JavaScript digital clock that uses our digits to display hours, minutes and seconds as hexadecimal numbers.


        Sunday, April 17, 2016

        A Cancel Button for somerby.net/mack/logic

        Good news: somerby.net/mack/logic now has a cancel button.  If a decision is taking too long, you can cancel it and continue working.  You don't have to close the browser anymore.

        Bad news: somerby.net/mack/logic is not working in Internet Explorer, or at least it isn't working in Internet Explorer 11 on my computer.  I'll try to fix it soon.

        It works for me in Chrome and Firefox.  I'd appreciate it if anyone tells me whether or not its working for them in other browsers.  Just leave a comment on this post.

        Monday, February 15, 2016

        A New Web App: "Expanding Quine's Definitions"

        I've been messing around with code that creates symbolic definitions of the number one for quite a while: these blog posts show some of the results.  All this messing around has culminated in a web app:
        http://somerby.net/mack/definitions/.  With it, you can expand Quine's definition of the number one interactively in various ways, and also many other of his definitions.  What fun!