Monthly Archives: February 2011

Several ways to prove a simple proposition

Posted on 2011/02/17 by Thomas Strathmann

Coq provides many tactics. In this post we show a number of proofs that use different tactics to prove a simple proposition of first order logic, namely which in Coq translates to forall P Q : Prop, P /\ Q … Continue reading →

Posted in Coq | Tagged | Leave a comment

Using Qucs for filter design

Posted on 2011/02/15 by Thomas Strathmann

Qucs, short for Quite Universal Circuit Simulator, is as the name suggests a simulation package for electronic circuits. It’s free and sports a nice graphical schematic capture interface. One of its many nice and useful features is the ability to … Continue reading →

Posted in Electronics, Tools | Tagged , | 3 Comments

WordPress blogging in LaTeX

Posted on 2011/02/11 by Thomas Strathmann

Just found an interesting resource about blogging in LaTeX using WordPress. Eric Finster at Curious Reasoning has put together a Python script that allows you to prepare blog posts in LaTeX and convert them to the proper format. Might come … Continue reading →

Posted in Tools | Tagged , | Leave a comment

Beginning Ltac

Posted on 2011/02/10 by Thomas Strathmann

One of the strong points of Coq is its powerful proof automation facility embodied in the tactic language . Instead of having to write new tactics in ML, compiling them, and jumping through all sorts of hoops in the process, … Continue reading →

Posted in Coq | Tagged | Leave a comment

How to draw commutative diagrams in LaTeX with TikZ

Posted on 2011/02/02 by Thomas Strathmann

Sooner or later everyone who uses LaTeX to typeset documents containing maths will encounter the problem of how to draw commutative diagrams. There are many packages, some general purpose other specialized for the task. An excellent survey of some of … Continue reading →

Posted in Mathematics, Tools | Tagged , , , | 24 Comments