Todd Wilson

I can also see the potential advantages of a tactic like this, but I want to add a few dissenting points. My preference has always been to make proof scripts...

This is probably not the place to discuss proof engineering, but when I have to deal with lemmas with many variables and many hypotheses involving these variables, I define new...

This was removed from the 2.0.4 release, but I wanted to add a few observations about context reasoning in the hopes that, when schemas are eventually revived, some of these...

I can't recall how tactics like apply and backchain report failure to find matches, but my general feeling is that any time an error message is generated when something fails...

I'm not sure about how importing would affect search, but I've thought for a long time (and first suggested to Andrew in 2009) that it would be very useful to...

Here is a list to get things started: - [ ] The "For those who aren't familiar with the logic" section should be expanded to include enough information for the...

I wasn't suggesting reorganizing the examples in any way; I think the current organization is just fine. I was just thinking that a title alone is not enough information for...

But Abella does report line numbers and character ranges on other types of errors, such as syntax errors and typing errors.

One useful model to keep in mind here might be Twelf. There, you can put certain stylized comments in your source that initiate certain checks on the specification as it...

Is there any plan to revamp the generation of html versions of developments? I'm re-building my PFPL development in Abella 2.0.6 and would like to make the whole thing available...